/[mojave]/metaprl/theories/s4lp/s4_logic.ml
ViewVC logotype

Diff of /metaprl/theories/s4lp/s4_logic.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 9651 by yegor, Wed Apr 5 15:12:37 2006 UTC revision 9652 by nogin, Tue Oct 31 05:33:38 2006 UTC
# Line 13  Line 13 
13     See the file doc/htmlman/default.html or visit http://metaprl.org/     See the file doc/htmlman/default.html or visit http://metaprl.org/
14     for more information.     for more information.
15    
16     Copyright (C) 1998 Jason Hickey, Cornell University     Copyright (C) 2005-2006 MetaPRL Group, Caltech
17    
18     This program is free software; you can redistribute it and/or     This program is free software; you can redistribute it and/or
19     modify it under the terms of the GNU General Public License     modify it under the terms of the GNU General Public License
# Line 151  Line 151 
151   * DISPLAY FORMS                                                        *   * DISPLAY FORMS                                                        *
152   ************************************************************************)   ************************************************************************)
153    
154    define iform simple_box: box{'a} <--> box[0]{'a}
155    define iform diamond : diamond[i:n]{'a} <--> "not"{"box"[i:n]{"not"{'a}}}
156    define iform simple_diamond : diamond{'a} <--> diamond[0]{'a}
157    define iform iff : "iff"{'a; 'b} <--> "and"{'a => 'b; 'b => 'a}
158    
159  prec prec_implies  prec prec_implies
160  prec prec_and  prec prec_and
161  prec prec_or  prec prec_or
# Line 186  Line 191 
191  dform implies_df3 : mode[src] :: mode[prl] :: mode[html] :: mode[tex] :: implies_df{'a} =  dform implies_df3 : mode[src] :: mode[prl] :: mode[html] :: mode[tex] :: implies_df{'a} =
192     hspace Mpsymbols!Rightarrow `" " slot{'a}     hspace Mpsymbols!Rightarrow `" " slot{'a}
193    
194    dform iff_df : parens :: "prec"[prec_implies] :: mode[prl] :: mode[html] :: mode[tex] :: "iff"{'a; 'b} =
195       szone pushm[0] slot["le"]{'a} Leftrightarrow slot["le"]{'b} popm ezone
196    
197  (*  (*
198   * Disjunction.   * Disjunction.
199   *)   *)
# Line 220  Line 228 
228  dform box_df1 : except_mode[src] :: parens :: "prec"[prec_not] :: box[i:n]{'a} =  dform box_df1 : except_mode[src] :: parens :: "prec"[prec_not] :: box[i:n]{'a} =
229     `"[" slot[i] `"]" slot["lt"]{'a}     `"[" slot[i] `"]" slot["lt"]{'a}
230    
231    dform box_df2 : except_mode[src] :: parens :: "prec"[prec_not] :: box{'a} =
232       Mpsymbols!box slot["lt"]{'a}
233    
234    dform diamond_df1 : except_mode[src] :: parens :: "prec"[prec_not] :: diamond[i:n]{'a} =
235       `"<" slot[i] `">" slot["lt"]{'a}
236    
237    dform diamond_df2 : except_mode[src] :: parens :: "prec"[prec_not] :: box{'a} =
238       `"<>" slot["lt"]{'a}
239    
240  dform sequent_df : sequent_arg = sub["S4nJ"]  dform sequent_df : sequent_arg = sub["S4nJ"]
241    
242  declare display_sequent{'s : Dform} : Dform  declare display_sequent{'s : Dform} : Dform

Legend:
Removed from v.9651  
changed lines
  Added in v.9652

  ViewVC Help
Powered by ViewVC 1.1.26