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

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

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

revision 9651 by yegor, Tue Jul 12 06:15:11 2005 UTC revision 9652 by nogin, Tue Oct 31 05:33:38 2006 UTC
# Line 10  Line 10 
10   * See the file doc/htmlman/default.html or visit http://metaprl.org/   * See the file doc/htmlman/default.html or visit http://metaprl.org/
11   * for more information.   * for more information.
12   *   *
13   * Copyright (C) 1998 Jason Hickey, Cornell University   * Copyright (C) 2005-2006 MetaPRL Group, Caltech
14   *   *
15   * This program is free software; you can redistribute it and/or   * This program is free software; you can redistribute it and/or
16   * modify it under the terms of the GNU General Public License   * modify it under the terms of the GNU General Public License
# Line 51  Line 51 
51  declare "or"{'a; 'b}  declare "or"{'a; 'b}
52  declare "implies"{'a; 'b}  declare "implies"{'a; 'b}
53  declare "box"[i:n]{'a}  declare "box"[i:n]{'a}
54    
55    define iform simple_box: box{'a} <--> box[0]{'a}
56    define iform diamond : diamond[i:n]{'a} <--> "not"{"box"[i:n]{"not"{'a}}}
57    define iform simple_diamond : diamond{'a} <--> diamond[0]{'a}
58    define iform iff : "iff"{'a; 'b} <--> "and"{'a => 'b; 'b => 'a}
59    
60  (************************************************************************  (************************************************************************
61   * DISPLAY FORMS                                                        *   * DISPLAY FORMS                                                        *
62   ************************************************************************)   ************************************************************************)
# Line 100  Line 106 
106  (*  (*
107   * -*-   * -*-
108   * Local Variables:   * Local Variables:
  * Caml-master: "prlcomp.run"  
109   * End:   * End:
110   * -*-   * -*-
111   *)   *)

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

  ViewVC Help
Powered by ViewVC 1.1.26