expanded tabs
authorclasohm
Mon Feb 05 14:44:09 1996 +0100 (1996-02-05)
changeset 14743f7d67927fe2
parent 1473 e8d4606e6502
child 1475 7f5a4cd08209
expanded tabs
src/CCL/CCL.thy
src/CCL/Fix.thy
src/CCL/Gfp.thy
src/CCL/Hered.thy
src/CCL/Lfp.thy
src/CCL/Term.thy
src/CCL/Trancl.thy
src/CCL/Type.thy
src/CCL/Wfd.thy
src/CCL/ex/Flag.thy
src/CCL/ex/List.thy
src/CCL/ex/Nat.thy
src/CCL/ex/Stream.thy
src/CTT/Arith.thy
src/CTT/Bool.thy
src/LCF/LCF.thy
src/LK/LK.thy
src/Modal/Modal0.thy
src/Modal/S4.thy
src/Modal/S43.thy
src/Modal/T.thy
     1.1 --- a/src/CCL/CCL.thy	Mon Feb 05 13:44:28 1996 +0100
     1.2 +++ b/src/CCL/CCL.thy	Mon Feb 05 14:44:09 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	CCL/ccl.thy
     1.5 +(*  Title:      CCL/ccl.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Martin Coen
     1.8 +    Author:     Martin Coen
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Classical Computational Logic for Untyped Lambda Calculus with reduction to 
     2.1 --- a/src/CCL/Fix.thy	Mon Feb 05 13:44:28 1996 +0100
     2.2 +++ b/src/CCL/Fix.thy	Mon Feb 05 14:44:09 1996 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4 -(*  Title: 	CCL/Lazy/fix.thy
     2.5 +(*  Title:      CCL/Lazy/fix.thy
     2.6      ID:         $Id$
     2.7 -    Author: 	Martin Coen
     2.8 +    Author:     Martin Coen
     2.9      Copyright   1993  University of Cambridge
    2.10  
    2.11  Tentative attempt at including fixed point induction.
    2.12 @@ -11,7 +11,7 @@
    2.13  
    2.14  consts
    2.15  
    2.16 -  idgen      ::	      "[i]=>i"
    2.17 +  idgen      ::       "[i]=>i"
    2.18    INCL      :: "[i=>o]=>o"
    2.19  
    2.20  rules
     3.1 --- a/src/CCL/Gfp.thy	Mon Feb 05 13:44:28 1996 +0100
     3.2 +++ b/src/CCL/Gfp.thy	Mon Feb 05 14:44:09 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title: 	HOL/gfp.thy
     3.5 +(*  Title:      HOL/gfp.thy
     3.6      ID:         $Id$
     3.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.9      Copyright   1992  University of Cambridge
    3.10  
    3.11  Greatest fixed points
     4.1 --- a/src/CCL/Hered.thy	Mon Feb 05 13:44:28 1996 +0100
     4.2 +++ b/src/CCL/Hered.thy	Mon Feb 05 14:44:09 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	CCL/hered.thy
     4.5 +(*  Title:      CCL/hered.thy
     4.6      ID:         $Id$
     4.7 -    Author: 	Martin Coen
     4.8 +    Author:     Martin Coen
     4.9      Copyright   1993  University of Cambridge
    4.10  
    4.11  Hereditary Termination - cf. Martin Lo\"f
     5.1 --- a/src/CCL/Lfp.thy	Mon Feb 05 13:44:28 1996 +0100
     5.2 +++ b/src/CCL/Lfp.thy	Mon Feb 05 14:44:09 1996 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4 -(*  Title: 	HOL/lfp.thy
     5.5 +(*  Title:      HOL/lfp.thy
     5.6      ID:         $Id$
     5.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.9      Copyright   1992  University of Cambridge
    5.10  
    5.11  The Knaster-Tarski Theorem
     6.1 --- a/src/CCL/Term.thy	Mon Feb 05 13:44:28 1996 +0100
     6.2 +++ b/src/CCL/Term.thy	Mon Feb 05 14:44:09 1996 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4 -(*  Title: 	CCL/terms.thy
     6.5 +(*  Title:      CCL/terms.thy
     6.6      ID:         $Id$
     6.7 -    Author: 	Martin Coen
     6.8 +    Author:     Martin Coen
     6.9      Copyright   1993  University of Cambridge
    6.10  
    6.11  Definitions of usual program constructs in CCL.
    6.12 @@ -38,16 +38,16 @@
    6.13    letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    6.14  
    6.15    "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
    6.16 -  			[0,0,60] 60)
    6.17 +                        [0,0,60] 60)
    6.18  
    6.19    "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    6.20 -  			[0,0,0,60] 60)
    6.21 +                        [0,0,0,60] 60)
    6.22  
    6.23    "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    6.24 -  			[0,0,0,0,60] 60)
    6.25 +                        [0,0,0,0,60] 60)
    6.26  
    6.27    "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    6.28 -  			[0,0,0,0,0,60] 60)
    6.29 +                        [0,0,0,0,0,60] 60)
    6.30  
    6.31    napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
    6.32  
    6.33 @@ -66,7 +66,7 @@
    6.34    succ_def               "succ(n) == inr(n)"
    6.35    ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
    6.36    nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
    6.37 -  nil_def	              "[] == inl(one)"
    6.38 +  nil_def                     "[] == inl(one)"
    6.39    cons_def                   "h$t == inr(<h,t>)"
    6.40    lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
    6.41    lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
     7.1 --- a/src/CCL/Trancl.thy	Mon Feb 05 13:44:28 1996 +0100
     7.2 +++ b/src/CCL/Trancl.thy	Mon Feb 05 14:44:09 1996 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4 -(*  Title: 	CCL/trancl.thy
     7.5 +(*  Title:      CCL/trancl.thy
     7.6      ID:         $Id$
     7.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     7.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     7.9      Copyright   1993  University of Cambridge
    7.10  
    7.11  Transitive closure of a relation
    7.12 @@ -9,20 +9,20 @@
    7.13  Trancl = CCL +
    7.14  
    7.15  consts
    7.16 -    trans   :: "i set => o" 	              (*transitivity predicate*)
    7.17 -    id	    :: "i set"
    7.18 -    rtrancl :: "i set => i set"	              ("(_^*)" [100] 100)
    7.19 -    trancl  :: "i set => i set"	              ("(_^+)" [100] 100)  
    7.20 -    O	    :: "[i set,i set] => i set"       (infixr 60)
    7.21 +    trans   :: "i set => o"                   (*transitivity predicate*)
    7.22 +    id      :: "i set"
    7.23 +    rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
    7.24 +    trancl  :: "i set => i set"               ("(_^+)" [100] 100)  
    7.25 +    O       :: "[i set,i set] => i set"       (infixr 60)
    7.26  
    7.27  rules   
    7.28  
    7.29 -trans_def	"trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    7.30 -comp_def	(*composition of relations*)
    7.31 -		"r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    7.32 -id_def		(*the identity relation*)
    7.33 -		"id == {p. EX x. p = <x,x>}"
    7.34 -rtrancl_def	"r^* == lfp(%s. id Un (r O s))"
    7.35 -trancl_def	"r^+ == r O rtrancl(r)"
    7.36 +trans_def       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    7.37 +comp_def        (*composition of relations*)
    7.38 +                "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
    7.39 +id_def          (*the identity relation*)
    7.40 +                "id == {p. EX x. p = <x,x>}"
    7.41 +rtrancl_def     "r^* == lfp(%s. id Un (r O s))"
    7.42 +trancl_def      "r^+ == r O rtrancl(r)"
    7.43  
    7.44  end
     8.1 --- a/src/CCL/Type.thy	Mon Feb 05 13:44:28 1996 +0100
     8.2 +++ b/src/CCL/Type.thy	Mon Feb 05 14:44:09 1996 +0100
     8.3 @@ -28,10 +28,10 @@
     8.4    SPLIT         :: "[i, [i, i] => i set] => i set"
     8.5  
     8.6    "@Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
     8.7 -  				[0,0,60] 60)
     8.8 +                                [0,0,60] 60)
     8.9  
    8.10    "@Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
    8.11 -  				[0,0,60] 60)
    8.12 +                                [0,0,60] 60)
    8.13    
    8.14    "@->"         :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
    8.15    "@*"          :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
     9.1 --- a/src/CCL/Wfd.thy	Mon Feb 05 13:44:28 1996 +0100
     9.2 +++ b/src/CCL/Wfd.thy	Mon Feb 05 14:44:09 1996 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4 -(*  Title: 	CCL/wfd.thy
     9.5 +(*  Title:      CCL/wfd.thy
     9.6      ID:         $Id$
     9.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     9.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     9.9      Copyright   1993  University of Cambridge
    9.10  
    9.11  Well-founded relations in CCL.
    10.1 --- a/src/CCL/ex/Flag.thy	Mon Feb 05 13:44:28 1996 +0100
    10.2 +++ b/src/CCL/ex/Flag.thy	Mon Feb 05 14:44:09 1996 +0100
    10.3 @@ -1,6 +1,6 @@
    10.4 -(*  Title: 	CCL/ex/flag.thy
    10.5 +(*  Title:      CCL/ex/flag.thy
    10.6      ID:         $Id$
    10.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    10.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    10.9      Copyright   1993  University of Cambridge
   10.10  
   10.11  Dutch national flag program - except that the point of Dijkstra's example was to use 
    11.1 --- a/src/CCL/ex/List.thy	Mon Feb 05 13:44:28 1996 +0100
    11.2 +++ b/src/CCL/ex/List.thy	Mon Feb 05 14:44:09 1996 +0100
    11.3 @@ -1,6 +1,6 @@
    11.4 -(*  Title: 	CCL/ex/list.thy
    11.5 +(*  Title:      CCL/ex/list.thy
    11.6      ID:         $Id$
    11.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    11.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    11.9      Copyright   1993  University of Cambridge
   11.10  
   11.11  Programs defined over lists.
    12.1 --- a/src/CCL/ex/Nat.thy	Mon Feb 05 13:44:28 1996 +0100
    12.2 +++ b/src/CCL/ex/Nat.thy	Mon Feb 05 14:44:09 1996 +0100
    12.3 @@ -1,6 +1,6 @@
    12.4 -(*  Title: 	CCL/ex/nat.thy
    12.5 +(*  Title:      CCL/ex/nat.thy
    12.6      ID:         $Id$
    12.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    12.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    12.9      Copyright   1993  University of Cambridge
   12.10  
   12.11  Programs defined over the natural numbers
    13.1 --- a/src/CCL/ex/Stream.thy	Mon Feb 05 13:44:28 1996 +0100
    13.2 +++ b/src/CCL/ex/Stream.thy	Mon Feb 05 14:44:09 1996 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4 -(*  Title: 	CCL/ex/stream.thy
    13.5 +(*  Title:      CCL/ex/stream.thy
    13.6      ID:         $Id$
    13.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    13.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    13.9      Copyright   1993  University of Cambridge
   13.10  
   13.11  Programs defined over streams.
    14.1 --- a/src/CTT/Arith.thy	Mon Feb 05 13:44:28 1996 +0100
    14.2 +++ b/src/CTT/Arith.thy	Mon Feb 05 14:44:09 1996 +0100
    14.3 @@ -1,6 +1,6 @@
    14.4 -(*  Title: 	CTT/arith
    14.5 +(*  Title:      CTT/arith
    14.6      ID:         $Id$
    14.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    14.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.9      Copyright   1991  University of Cambridge
   14.10  
   14.11  Arithmetic operators and their definitions
   14.12 @@ -11,8 +11,8 @@
   14.13  
   14.14  Arith = CTT +
   14.15  
   14.16 -consts "#+","-","|-|"	:: "[i,i]=>i"	(infixr 65)
   14.17 -       "#*",div,mod     :: "[i,i]=>i"	(infixr 70)
   14.18 +consts "#+","-","|-|"   :: "[i,i]=>i"   (infixr 65)
   14.19 +       "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
   14.20  
   14.21  rules
   14.22    add_def     "a#+b == rec(a, b, %u v.succ(v))"  
    15.1 --- a/src/CTT/Bool.thy	Mon Feb 05 13:44:28 1996 +0100
    15.2 +++ b/src/CTT/Bool.thy	Mon Feb 05 14:44:09 1996 +0100
    15.3 @@ -1,6 +1,6 @@
    15.4 -(*  Title: 	CTT/bool
    15.5 +(*  Title:      CTT/bool
    15.6      ID:         $Id$
    15.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    15.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.9      Copyright   1991  University of Cambridge
   15.10  
   15.11  The two-element type (booleans and conditionals)
   15.12 @@ -8,12 +8,12 @@
   15.13  
   15.14  Bool = CTT +
   15.15  
   15.16 -consts Bool		:: "t"
   15.17 -       true,false	:: "i"
   15.18 -       cond		:: "[i,i,i]=>i"
   15.19 +consts Bool             :: "t"
   15.20 +       true,false       :: "i"
   15.21 +       cond             :: "[i,i,i]=>i"
   15.22  rules
   15.23 -  Bool_def	"Bool == T+T"
   15.24 -  true_def	"true == inl(tt)"
   15.25 -  false_def	"false == inr(tt)"
   15.26 -  cond_def	"cond(a,b,c) == when(a, %u.b, %u.c)"
   15.27 +  Bool_def      "Bool == T+T"
   15.28 +  true_def      "true == inl(tt)"
   15.29 +  false_def     "false == inr(tt)"
   15.30 +  cond_def      "cond(a,b,c) == when(a, %u.b, %u.c)"
   15.31  end
    16.1 --- a/src/LCF/LCF.thy	Mon Feb 05 13:44:28 1996 +0100
    16.2 +++ b/src/LCF/LCF.thy	Mon Feb 05 14:44:09 1996 +0100
    16.3 @@ -1,6 +1,6 @@
    16.4 -(*  Title: 	LCF/lcf.thy
    16.5 +(*  Title:      LCF/lcf.thy
    16.6      ID:         $Id$
    16.7 -    Author: 	Tobias Nipkow
    16.8 +    Author:     Tobias Nipkow
    16.9      Copyright   1992  University of Cambridge
   16.10  
   16.11  Natural Deduction Rules for LCF
   16.12 @@ -15,61 +15,61 @@
   16.13  types
   16.14   tr
   16.15   void
   16.16 - ('a,'b) "*"		(infixl 6)
   16.17 - ('a,'b) "+"		(infixl 5)
   16.18 + ('a,'b) "*"            (infixl 6)
   16.19 + ('a,'b) "+"            (infixl 5)
   16.20  
   16.21  arities
   16.22   fun, "*", "+" :: (cpo,cpo)cpo
   16.23   tr,void       :: cpo
   16.24  
   16.25  consts
   16.26 - UU	:: "'a"
   16.27 - TT,FF	:: "tr"
   16.28 - FIX	:: "('a => 'a) => 'a"
   16.29 - FST	:: "'a*'b => 'a"
   16.30 - SND	:: "'a*'b => 'b"
   16.31 + UU     :: "'a"
   16.32 + TT,FF  :: "tr"
   16.33 + FIX    :: "('a => 'a) => 'a"
   16.34 + FST    :: "'a*'b => 'a"
   16.35 + SND    :: "'a*'b => 'b"
   16.36   INL    :: "'a => 'a+'b"
   16.37   INR    :: "'b => 'a+'b"
   16.38   WHEN   :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
   16.39 - adm	:: "('a => o) => o"
   16.40 - VOID	:: "void"		("'(')")
   16.41 - PAIR	:: "['a,'b] => 'a*'b"	("(1<_,/_>)" [0,0] 100)
   16.42 - COND	:: "[tr,'a,'a] => 'a"	("(_ =>/ (_ |/ _))" [60,60,60] 60)
   16.43 - "<<"	:: "['a,'a] => o"	(infixl 50)
   16.44 + adm    :: "('a => o) => o"
   16.45 + VOID   :: "void"               ("'(')")
   16.46 + PAIR   :: "['a,'b] => 'a*'b"   ("(1<_,/_>)" [0,0] 100)
   16.47 + COND   :: "[tr,'a,'a] => 'a"   ("(_ =>/ (_ |/ _))" [60,60,60] 60)
   16.48 + "<<"   :: "['a,'a] => o"       (infixl 50)
   16.49  rules
   16.50    (** DOMAIN THEORY **)
   16.51  
   16.52 -  eq_def	"x=y == x << y & y << x"
   16.53 +  eq_def        "x=y == x << y & y << x"
   16.54  
   16.55 -  less_trans	"[| x << y; y << z |] ==> x << z"
   16.56 +  less_trans    "[| x << y; y << z |] ==> x << z"
   16.57  
   16.58 -  less_ext	"(ALL x. f(x) << g(x)) ==> f << g"
   16.59 +  less_ext      "(ALL x. f(x) << g(x)) ==> f << g"
   16.60  
   16.61 -  mono		"[| f << g; x << y |] ==> f(x) << g(y)"
   16.62 +  mono          "[| f << g; x << y |] ==> f(x) << g(y)"
   16.63  
   16.64 -  minimal	"UU << x"
   16.65 +  minimal       "UU << x"
   16.66  
   16.67 -  FIX_eq	"f(FIX(f)) = FIX(f)"
   16.68 +  FIX_eq        "f(FIX(f)) = FIX(f)"
   16.69  
   16.70    (** TR **)
   16.71  
   16.72 -  tr_cases	"p=UU | p=TT | p=FF"
   16.73 +  tr_cases      "p=UU | p=TT | p=FF"
   16.74  
   16.75    not_TT_less_FF "~ TT << FF"
   16.76    not_FF_less_TT "~ FF << TT"
   16.77    not_TT_less_UU "~ TT << UU"
   16.78    not_FF_less_UU "~ FF << UU"
   16.79  
   16.80 -  COND_UU	"UU => x | y  =  UU"
   16.81 -  COND_TT	"TT => x | y  =  x"
   16.82 -  COND_FF	"FF => x | y  =  y"
   16.83 +  COND_UU       "UU => x | y  =  UU"
   16.84 +  COND_TT       "TT => x | y  =  x"
   16.85 +  COND_FF       "FF => x | y  =  y"
   16.86  
   16.87    (** PAIRS **)
   16.88  
   16.89 -  surj_pairing	"<FST(z),SND(z)> = z"
   16.90 +  surj_pairing  "<FST(z),SND(z)> = z"
   16.91  
   16.92 -  FST	"FST(<x,y>) = x"
   16.93 -  SND	"SND(<x,y>) = y"
   16.94 +  FST   "FST(<x,y>) = x"
   16.95 +  SND   "SND(<x,y>) = y"
   16.96  
   16.97    (*** STRICT SUM ***)
   16.98  
   16.99 @@ -88,23 +88,23 @@
  16.100  
  16.101    (** VOID **)
  16.102  
  16.103 -  void_cases	"(x::void) = UU"
  16.104 +  void_cases    "(x::void) = UU"
  16.105  
  16.106    (** INDUCTION **)
  16.107  
  16.108 -  induct	"[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
  16.109 +  induct        "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
  16.110  
  16.111    (** Admissibility / Chain Completeness **)
  16.112    (* All rules can be found on pages 199--200 of Larry's LCF book.
  16.113       Note that "easiness" of types is not taken into account
  16.114       because it cannot be expressed schematically; flatness could be. *)
  16.115  
  16.116 -  adm_less	"adm(%x.t(x) << u(x))"
  16.117 -  adm_not_less	"adm(%x.~ t(x) << u)"
  16.118 +  adm_less      "adm(%x.t(x) << u(x))"
  16.119 +  adm_not_less  "adm(%x.~ t(x) << u)"
  16.120    adm_not_free  "adm(%x.A)"
  16.121 -  adm_subst	"adm(P) ==> adm(%x.P(t(x)))"
  16.122 -  adm_conj	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
  16.123 -  adm_disj	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
  16.124 -  adm_imp	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
  16.125 -  adm_all	"(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
  16.126 +  adm_subst     "adm(P) ==> adm(%x.P(t(x)))"
  16.127 +  adm_conj      "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
  16.128 +  adm_disj      "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
  16.129 +  adm_imp       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
  16.130 +  adm_all       "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
  16.131  end
    17.1 --- a/src/LK/LK.thy	Mon Feb 05 13:44:28 1996 +0100
    17.2 +++ b/src/LK/LK.thy	Mon Feb 05 14:44:09 1996 +0100
    17.3 @@ -1,6 +1,6 @@
    17.4 -(*  Title: 	LK/lk.thy
    17.5 +(*  Title:      LK/lk.thy
    17.6      ID:         $Id$
    17.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    17.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.9      Copyright   1993  University of Cambridge
   17.10  
   17.11  Classical First-Order Sequent Calculus
   17.12 @@ -19,51 +19,51 @@
   17.13   o :: logic
   17.14  
   17.15  consts
   17.16 - True,False	:: "o"
   17.17 - "="		:: "['a,'a] => o"	(infixl 50)
   17.18 - "Not"		:: "o => o"		("~ _" [40] 40)
   17.19 - "&"		:: "[o,o] => o"		(infixr 35)
   17.20 - "|"		:: "[o,o] => o"		(infixr 30)
   17.21 - "-->","<->"	:: "[o,o] => o"		(infixr 25)
   17.22 - The		:: "('a => o) => 'a"	(binder "THE " 10)
   17.23 - All		:: "('a => o) => o"	(binder "ALL " 10)
   17.24 - Ex		:: "('a => o) => o"	(binder "EX " 10)
   17.25 + True,False     :: "o"
   17.26 + "="            :: "['a,'a] => o"       (infixl 50)
   17.27 + "Not"          :: "o => o"             ("~ _" [40] 40)
   17.28 + "&"            :: "[o,o] => o"         (infixr 35)
   17.29 + "|"            :: "[o,o] => o"         (infixr 30)
   17.30 + "-->","<->"    :: "[o,o] => o"         (infixr 25)
   17.31 + The            :: "('a => o) => 'a"    (binder "THE " 10)
   17.32 + All            :: "('a => o) => o"     (binder "ALL " 10)
   17.33 + Ex             :: "('a => o) => o"     (binder "EX " 10)
   17.34  
   17.35   (*Representation of sequents*)
   17.36 - Trueprop	:: "[sobj=>sobj,sobj=>sobj] => prop"
   17.37 - Seqof		:: "o => sobj=>sobj"
   17.38 - "@Trueprop"	:: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
   17.39 - "@MtSeq"	:: "sequence"				("" [] 1000)
   17.40 - "@NmtSeq"	:: "[seqobj,seqcont] => sequence"	("__" [] 1000)
   17.41 - "@MtSeqCont"	:: "seqcont"				("" [] 1000)
   17.42 - "@SeqCont"	:: "[seqobj,seqcont] => seqcont"	(",/ __" [] 1000)
   17.43 - ""		:: "o => seqobj"			("_" [] 1000)
   17.44 - "@SeqId"	:: "id => seqobj"			("$_" [] 1000)
   17.45 - "@SeqVar"	:: "var => seqobj"			("$_")
   17.46 + Trueprop       :: "[sobj=>sobj,sobj=>sobj] => prop"
   17.47 + Seqof          :: "o => sobj=>sobj"
   17.48 + "@Trueprop"    :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
   17.49 + "@MtSeq"       :: "sequence"                           ("" [] 1000)
   17.50 + "@NmtSeq"      :: "[seqobj,seqcont] => sequence"       ("__" [] 1000)
   17.51 + "@MtSeqCont"   :: "seqcont"                            ("" [] 1000)
   17.52 + "@SeqCont"     :: "[seqobj,seqcont] => seqcont"        (",/ __" [] 1000)
   17.53 + ""             :: "o => seqobj"                        ("_" [] 1000)
   17.54 + "@SeqId"       :: "id => seqobj"                       ("$_" [] 1000)
   17.55 + "@SeqVar"      :: "var => seqobj"                      ("$_")
   17.56  
   17.57  rules
   17.58    (*Structural rules*)
   17.59  
   17.60 -  basic	"$H, P, $G |- $E, P, $F"
   17.61 +  basic "$H, P, $G |- $E, P, $F"
   17.62  
   17.63 -  thinR	"$H |- $E, $F ==> $H |- $E, P, $F"
   17.64 -  thinL	"$H, $G |- $E ==> $H, P, $G |- $E"
   17.65 +  thinR "$H |- $E, $F ==> $H |- $E, P, $F"
   17.66 +  thinL "$H, $G |- $E ==> $H, P, $G |- $E"
   17.67  
   17.68 -  cut	"[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
   17.69 +  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
   17.70  
   17.71    (*Propositional rules*)
   17.72  
   17.73 -  conjR	"[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
   17.74 -  conjL	"$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
   17.75 +  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
   17.76 +  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
   17.77  
   17.78 -  disjR	"$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
   17.79 -  disjL	"[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
   17.80 +  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
   17.81 +  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
   17.82  
   17.83 -  impR	"$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
   17.84 -  impL	"[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
   17.85 +  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
   17.86 +  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
   17.87  
   17.88 -  notR	"$H, P |- $E, $F ==> $H |- $E, ~P, $F"
   17.89 -  notL	"$H, $G |- $E, P ==> $H, ~P, $G |- $E"
   17.90 +  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
   17.91 +  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
   17.92  
   17.93    FalseL "$H, False, $G |- $E"
   17.94  
   17.95 @@ -72,15 +72,15 @@
   17.96  
   17.97    (*Quantifiers*)
   17.98  
   17.99 -  allR	"(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
  17.100 -  allL	"$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
  17.101 +  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
  17.102 +  allL  "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
  17.103  
  17.104 -  exR	"$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
  17.105 -  exL	"(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
  17.106 +  exR   "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
  17.107 +  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
  17.108  
  17.109    (*Equality*)
  17.110  
  17.111 -  refl	"$H |- $E, a=a, $F"
  17.112 +  refl  "$H |- $E, a=a, $F"
  17.113    sym   "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
  17.114    trans "[| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
  17.115  
    18.1 --- a/src/Modal/Modal0.thy	Mon Feb 05 13:44:28 1996 +0100
    18.2 +++ b/src/Modal/Modal0.thy	Mon Feb 05 14:44:09 1996 +0100
    18.3 @@ -1,24 +1,24 @@
    18.4 -(*  Title: 	91/Modal/modal0
    18.5 +(*  Title:      91/Modal/modal0
    18.6      ID:         $Id$
    18.7 -    Author: 	Martin Coen
    18.8 +    Author:     Martin Coen
    18.9      Copyright   1991  University of Cambridge
   18.10  *)
   18.11  
   18.12  Modal0 = LK +
   18.13  
   18.14  consts
   18.15 -  box		:: "o=>o"	("[]_" [50] 50)
   18.16 -  dia		:: "o=>o"	("<>_" [50] 50)
   18.17 -  "--<",">-<"	:: "[o,o]=>o"	(infixr 25)
   18.18 -  "@Lstar"	:: "[sequence,sequence]=>prop"	("(_)|L>(_)" [6,6] 5)
   18.19 -  "@Rstar"	:: "[sequence,sequence]=>prop"	("(_)|R>(_)" [6,6] 5)
   18.20 -  Lstar,Rstar	:: "[sobj=>sobj,sobj=>sobj]=>prop"
   18.21 +  box           :: "o=>o"       ("[]_" [50] 50)
   18.22 +  dia           :: "o=>o"       ("<>_" [50] 50)
   18.23 +  "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
   18.24 +  "@Lstar"      :: "[sequence,sequence]=>prop"  ("(_)|L>(_)" [6,6] 5)
   18.25 +  "@Rstar"      :: "[sequence,sequence]=>prop"  ("(_)|R>(_)" [6,6] 5)
   18.26 +  Lstar,Rstar   :: "[sobj=>sobj,sobj=>sobj]=>prop"
   18.27  
   18.28  rules
   18.29    (* Definitions *)
   18.30  
   18.31 -  strimp_def	"P --< Q == [](P --> Q)"
   18.32 -  streqv_def	"P >-< Q == (P --< Q) & (Q --< P)"
   18.33 +  strimp_def    "P --< Q == [](P --> Q)"
   18.34 +  streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
   18.35  end
   18.36  
   18.37  ML
    19.1 --- a/src/Modal/S4.thy	Mon Feb 05 13:44:28 1996 +0100
    19.2 +++ b/src/Modal/S4.thy	Mon Feb 05 14:44:09 1996 +0100
    19.3 @@ -1,6 +1,6 @@
    19.4 -(*  Title: 	91/Modal/S4
    19.5 +(*  Title:      91/Modal/S4
    19.6      ID:         $Id$
    19.7 -    Author: 	Martin Coen
    19.8 +    Author:     Martin Coen
    19.9      Copyright   1991  University of Cambridge
   19.10  *)
   19.11  
    20.1 --- a/src/Modal/S43.thy	Mon Feb 05 13:44:28 1996 +0100
    20.2 +++ b/src/Modal/S43.thy	Mon Feb 05 14:44:09 1996 +0100
    20.3 @@ -1,6 +1,6 @@
    20.4 -(*  Title: 	91/Modal/S43
    20.5 +(*  Title:      91/Modal/S43
    20.6      ID:         $Id$
    20.7 -    Author: 	Martin Coen
    20.8 +    Author:     Martin Coen
    20.9      Copyright   1991  University of Cambridge
   20.10  
   20.11  This implements Rajeev Gore's sequent calculus for S43.
   20.12 @@ -9,10 +9,10 @@
   20.13  S43 = Modal0 +
   20.14  
   20.15  consts
   20.16 -  S43pi	:: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,
   20.17 -	     sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
   20.18 +  S43pi :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,
   20.19 +             sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
   20.20    "@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,
   20.21 -		sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
   20.22 +                sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
   20.23  
   20.24  rules
   20.25  (* Definition of the star operation using a set of Horn clauses  *)
   20.26 @@ -69,9 +69,9 @@
   20.27    val tr' = LK.seq_tr1';
   20.28  
   20.29    fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
   20.30 -	Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
   20.31 +        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
   20.32    fun s43pi_tr'[Abs(_,_,s1),Abs(_,_,s2),Abs(_,_,s3),
   20.33 -		Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] =
   20.34 +                Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] =
   20.35          Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
   20.36  in
   20.37  val parse_translation = [(SS43pi,s43pi_tr)];
    21.1 --- a/src/Modal/T.thy	Mon Feb 05 13:44:28 1996 +0100
    21.2 +++ b/src/Modal/T.thy	Mon Feb 05 14:44:09 1996 +0100
    21.3 @@ -1,6 +1,6 @@
    21.4 -(*  Title: 	91/Modal/T
    21.5 +(*  Title:      91/Modal/T
    21.6      ID:         $Id$
    21.7 -    Author: 	Martin Coen
    21.8 +    Author:     Martin Coen
    21.9      Copyright   1991  University of Cambridge
   21.10  *)
   21.11