/[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 9652 by nogin, Tue Oct 31 05:33:38 2006 UTC revision 9653 by nogin, Tue Oct 31 05:41:14 2006 UTC
# Line 234  Line 234 
234  dform diamond_df1 : except_mode[src] :: parens :: "prec"[prec_not] :: diamond[i:n]{'a} =  dform diamond_df1 : except_mode[src] :: parens :: "prec"[prec_not] :: diamond[i:n]{'a} =
235     `"<" slot[i] `">" slot["lt"]{'a}     `"<" slot[i] `">" slot["lt"]{'a}
236    
237  dform diamond_df2 : except_mode[src] :: parens :: "prec"[prec_not] :: box{'a} =  dform diamond_df2 : except_mode[src] :: parens :: "prec"[prec_not] :: diamond{'a} =
238     `"<>" slot["lt"]{'a}     `"<>" slot["lt"]{'a}
239    
240  dform sequent_df : sequent_arg = sub["S4nJ"]  dform sequent_df : sequent_arg = sub["S4nJ"]

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

  ViewVC Help
Powered by ViewVC 1.1.26