/[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 9654 by nogin, Tue Oct 31 05:41:14 2006 UTC revision 9655 by nogin, Tue Oct 31 18:16:04 2006 UTC
# Line 235  Line 235 
235     `"<" slot[i] `">" slot["lt"]{'a}     `"<" slot[i] `">" slot["lt"]{'a}
236    
237  dform diamond_df2 : except_mode[src] :: parens :: "prec"[prec_not] :: diamond{'a} =  dform diamond_df2 : except_mode[src] :: parens :: "prec"[prec_not] :: diamond{'a} =
238     `"<>" slot["lt"]{'a}     Mpsymbols!diamond slot["lt"]{'a}
239    
240  dform sequent_df : sequent_arg = sub["S4nJ"]  dform sequent_df : sequent_arg = sub["S4nJ"]
241    

Legend:
Removed from v.9654  
changed lines
  Added in v.9655

  ViewVC Help
Powered by ViewVC 1.1.26