--- a/src/CCL/CCL.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/CCL.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ccl.thy
+(* Title: CCL/ccl.thy
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1993 University of Cambridge
Classical Computational Logic for Untyped Lambda Calculus with reduction to
--- a/src/CCL/Fix.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Fix.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/Lazy/fix.thy
+(* Title: CCL/Lazy/fix.thy
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1993 University of Cambridge
Tentative attempt at including fixed point induction.
@@ -11,7 +11,7 @@
consts
- idgen :: "[i]=>i"
+ idgen :: "[i]=>i"
INCL :: "[i=>o]=>o"
rules
--- a/src/CCL/Gfp.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Gfp.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/gfp.thy
+(* Title: HOL/gfp.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Greatest fixed points
--- a/src/CCL/Hered.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Hered.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/hered.thy
+(* Title: CCL/hered.thy
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1993 University of Cambridge
Hereditary Termination - cf. Martin Lo\"f
--- a/src/CCL/Lfp.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Lfp.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/lfp.thy
+(* Title: HOL/lfp.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
The Knaster-Tarski Theorem
--- a/src/CCL/Term.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Term.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/terms.thy
+(* Title: CCL/terms.thy
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1993 University of Cambridge
Definitions of usual program constructs in CCL.
@@ -38,16 +38,16 @@
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
"@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)"
- [0,0,60] 60)
+ [0,0,60] 60)
"@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)"
- [0,0,0,60] 60)
+ [0,0,0,60] 60)
"@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)"
- [0,0,0,0,60] 60)
+ [0,0,0,0,60] 60)
"@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
- [0,0,0,0,0,60] 60)
+ [0,0,0,0,0,60] 60)
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
@@ -66,7 +66,7 @@
succ_def "succ(n) == inr(n)"
ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
- nil_def "[] == inl(one)"
+ nil_def "[] == inl(one)"
cons_def "h$t == inr(<h,t>)"
lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
--- a/src/CCL/Trancl.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Trancl.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/trancl.thy
+(* Title: CCL/trancl.thy
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Transitive closure of a relation
@@ -9,20 +9,20 @@
Trancl = CCL +
consts
- trans :: "i set => o" (*transitivity predicate*)
- id :: "i set"
- rtrancl :: "i set => i set" ("(_^*)" [100] 100)
- trancl :: "i set => i set" ("(_^+)" [100] 100)
- O :: "[i set,i set] => i set" (infixr 60)
+ trans :: "i set => o" (*transitivity predicate*)
+ id :: "i set"
+ rtrancl :: "i set => i set" ("(_^*)" [100] 100)
+ trancl :: "i set => i set" ("(_^+)" [100] 100)
+ O :: "[i set,i set] => i set" (infixr 60)
rules
-trans_def "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
-comp_def (*composition of relations*)
- "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
-id_def (*the identity relation*)
- "id == {p. EX x. p = <x,x>}"
-rtrancl_def "r^* == lfp(%s. id Un (r O s))"
-trancl_def "r^+ == r O rtrancl(r)"
+trans_def "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+comp_def (*composition of relations*)
+ "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+id_def (*the identity relation*)
+ "id == {p. EX x. p = <x,x>}"
+rtrancl_def "r^* == lfp(%s. id Un (r O s))"
+trancl_def "r^+ == r O rtrancl(r)"
end
--- a/src/CCL/Type.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Type.thy Mon Feb 05 14:44:09 1996 +0100
@@ -28,10 +28,10 @@
SPLIT :: "[i, [i, i] => i set] => i set"
"@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)"
- [0,0,60] 60)
+ [0,0,60] 60)
"@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)"
- [0,0,60] 60)
+ [0,0,60] 60)
"@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53)
"@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55)
--- a/src/CCL/Wfd.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/Wfd.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/wfd.thy
+(* Title: CCL/wfd.thy
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Well-founded relations in CCL.
--- a/src/CCL/ex/Flag.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/ex/Flag.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/flag.thy
+(* Title: CCL/ex/flag.thy
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Dutch national flag program - except that the point of Dijkstra's example was to use
--- a/src/CCL/ex/List.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/ex/List.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/list.thy
+(* Title: CCL/ex/list.thy
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Programs defined over lists.
--- a/src/CCL/ex/Nat.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/ex/Nat.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/nat.thy
+(* Title: CCL/ex/nat.thy
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Programs defined over the natural numbers
--- a/src/CCL/ex/Stream.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CCL/ex/Stream.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CCL/ex/stream.thy
+(* Title: CCL/ex/stream.thy
ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Programs defined over streams.
--- a/src/CTT/Arith.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CTT/Arith.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/arith
+(* Title: CTT/arith
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Arithmetic operators and their definitions
@@ -11,8 +11,8 @@
Arith = CTT +
-consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65)
- "#*",div,mod :: "[i,i]=>i" (infixr 70)
+consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65)
+ "#*",div,mod :: "[i,i]=>i" (infixr 70)
rules
add_def "a#+b == rec(a, b, %u v.succ(v))"
--- a/src/CTT/Bool.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/CTT/Bool.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/bool
+(* Title: CTT/bool
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
The two-element type (booleans and conditionals)
@@ -8,12 +8,12 @@
Bool = CTT +
-consts Bool :: "t"
- true,false :: "i"
- cond :: "[i,i,i]=>i"
+consts Bool :: "t"
+ true,false :: "i"
+ cond :: "[i,i,i]=>i"
rules
- Bool_def "Bool == T+T"
- true_def "true == inl(tt)"
- false_def "false == inr(tt)"
- cond_def "cond(a,b,c) == when(a, %u.b, %u.c)"
+ Bool_def "Bool == T+T"
+ true_def "true == inl(tt)"
+ false_def "false == inr(tt)"
+ cond_def "cond(a,b,c) == when(a, %u.b, %u.c)"
end
--- a/src/LCF/LCF.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/LCF/LCF.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: LCF/lcf.thy
+(* Title: LCF/lcf.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1992 University of Cambridge
Natural Deduction Rules for LCF
@@ -15,61 +15,61 @@
types
tr
void
- ('a,'b) "*" (infixl 6)
- ('a,'b) "+" (infixl 5)
+ ('a,'b) "*" (infixl 6)
+ ('a,'b) "+" (infixl 5)
arities
fun, "*", "+" :: (cpo,cpo)cpo
tr,void :: cpo
consts
- UU :: "'a"
- TT,FF :: "tr"
- FIX :: "('a => 'a) => 'a"
- FST :: "'a*'b => 'a"
- SND :: "'a*'b => 'b"
+ UU :: "'a"
+ TT,FF :: "tr"
+ FIX :: "('a => 'a) => 'a"
+ FST :: "'a*'b => 'a"
+ SND :: "'a*'b => 'b"
INL :: "'a => 'a+'b"
INR :: "'b => 'a+'b"
WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
- adm :: "('a => o) => o"
- VOID :: "void" ("'(')")
- PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100)
- COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60)
- "<<" :: "['a,'a] => o" (infixl 50)
+ adm :: "('a => o) => o"
+ VOID :: "void" ("'(')")
+ PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100)
+ COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60)
+ "<<" :: "['a,'a] => o" (infixl 50)
rules
(** DOMAIN THEORY **)
- eq_def "x=y == x << y & y << x"
+ eq_def "x=y == x << y & y << x"
- less_trans "[| x << y; y << z |] ==> x << z"
+ less_trans "[| x << y; y << z |] ==> x << z"
- less_ext "(ALL x. f(x) << g(x)) ==> f << g"
+ less_ext "(ALL x. f(x) << g(x)) ==> f << g"
- mono "[| f << g; x << y |] ==> f(x) << g(y)"
+ mono "[| f << g; x << y |] ==> f(x) << g(y)"
- minimal "UU << x"
+ minimal "UU << x"
- FIX_eq "f(FIX(f)) = FIX(f)"
+ FIX_eq "f(FIX(f)) = FIX(f)"
(** TR **)
- tr_cases "p=UU | p=TT | p=FF"
+ tr_cases "p=UU | p=TT | p=FF"
not_TT_less_FF "~ TT << FF"
not_FF_less_TT "~ FF << TT"
not_TT_less_UU "~ TT << UU"
not_FF_less_UU "~ FF << UU"
- COND_UU "UU => x | y = UU"
- COND_TT "TT => x | y = x"
- COND_FF "FF => x | y = y"
+ COND_UU "UU => x | y = UU"
+ COND_TT "TT => x | y = x"
+ COND_FF "FF => x | y = y"
(** PAIRS **)
- surj_pairing "<FST(z),SND(z)> = z"
+ surj_pairing "<FST(z),SND(z)> = z"
- FST "FST(<x,y>) = x"
- SND "SND(<x,y>) = y"
+ FST "FST(<x,y>) = x"
+ SND "SND(<x,y>) = y"
(*** STRICT SUM ***)
@@ -88,23 +88,23 @@
(** VOID **)
- void_cases "(x::void) = UU"
+ void_cases "(x::void) = UU"
(** INDUCTION **)
- induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
+ induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
(** Admissibility / Chain Completeness **)
(* All rules can be found on pages 199--200 of Larry's LCF book.
Note that "easiness" of types is not taken into account
because it cannot be expressed schematically; flatness could be. *)
- adm_less "adm(%x.t(x) << u(x))"
- adm_not_less "adm(%x.~ t(x) << u)"
+ adm_less "adm(%x.t(x) << u(x))"
+ adm_not_less "adm(%x.~ t(x) << u)"
adm_not_free "adm(%x.A)"
- adm_subst "adm(P) ==> adm(%x.P(t(x)))"
- adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
- adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
- adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
- adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
+ adm_subst "adm(P) ==> adm(%x.P(t(x)))"
+ adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
+ adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
+ adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
+ adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
end
--- a/src/LK/LK.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/LK/LK.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: LK/lk.thy
+(* Title: LK/lk.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Classical First-Order Sequent Calculus
@@ -19,51 +19,51 @@
o :: logic
consts
- True,False :: "o"
- "=" :: "['a,'a] => o" (infixl 50)
- "Not" :: "o => o" ("~ _" [40] 40)
- "&" :: "[o,o] => o" (infixr 35)
- "|" :: "[o,o] => o" (infixr 30)
- "-->","<->" :: "[o,o] => o" (infixr 25)
- The :: "('a => o) => 'a" (binder "THE " 10)
- All :: "('a => o) => o" (binder "ALL " 10)
- Ex :: "('a => o) => o" (binder "EX " 10)
+ True,False :: "o"
+ "=" :: "['a,'a] => o" (infixl 50)
+ "Not" :: "o => o" ("~ _" [40] 40)
+ "&" :: "[o,o] => o" (infixr 35)
+ "|" :: "[o,o] => o" (infixr 30)
+ "-->","<->" :: "[o,o] => o" (infixr 25)
+ The :: "('a => o) => 'a" (binder "THE " 10)
+ All :: "('a => o) => o" (binder "ALL " 10)
+ Ex :: "('a => o) => o" (binder "EX " 10)
(*Representation of sequents*)
- Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop"
- Seqof :: "o => sobj=>sobj"
- "@Trueprop" :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
- "@MtSeq" :: "sequence" ("" [] 1000)
- "@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000)
- "@MtSeqCont" :: "seqcont" ("" [] 1000)
- "@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000)
- "" :: "o => seqobj" ("_" [] 1000)
- "@SeqId" :: "id => seqobj" ("$_" [] 1000)
- "@SeqVar" :: "var => seqobj" ("$_")
+ Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop"
+ Seqof :: "o => sobj=>sobj"
+ "@Trueprop" :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
+ "@MtSeq" :: "sequence" ("" [] 1000)
+ "@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000)
+ "@MtSeqCont" :: "seqcont" ("" [] 1000)
+ "@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000)
+ "" :: "o => seqobj" ("_" [] 1000)
+ "@SeqId" :: "id => seqobj" ("$_" [] 1000)
+ "@SeqVar" :: "var => seqobj" ("$_")
rules
(*Structural rules*)
- basic "$H, P, $G |- $E, P, $F"
+ basic "$H, P, $G |- $E, P, $F"
- thinR "$H |- $E, $F ==> $H |- $E, P, $F"
- thinL "$H, $G |- $E ==> $H, P, $G |- $E"
+ thinR "$H |- $E, $F ==> $H |- $E, P, $F"
+ thinL "$H, $G |- $E ==> $H, P, $G |- $E"
- cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E"
+ cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E"
(*Propositional rules*)
- conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
- conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
+ conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
+ conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
- disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
- disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
+ disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
+ disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
- impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
- impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
+ impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
+ impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
- notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
- notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
+ notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
+ notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
FalseL "$H, False, $G |- $E"
@@ -72,15 +72,15 @@
(*Quantifiers*)
- allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
- allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
+ allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
+ allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
- exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
- exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
+ exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
+ exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
(*Equality*)
- refl "$H |- $E, a=a, $F"
+ refl "$H |- $E, a=a, $F"
sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
--- a/src/Modal/Modal0.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/Modal/Modal0.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,24 +1,24 @@
-(* Title: 91/Modal/modal0
+(* Title: 91/Modal/modal0
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1991 University of Cambridge
*)
Modal0 = LK +
consts
- box :: "o=>o" ("[]_" [50] 50)
- dia :: "o=>o" ("<>_" [50] 50)
- "--<",">-<" :: "[o,o]=>o" (infixr 25)
- "@Lstar" :: "[sequence,sequence]=>prop" ("(_)|L>(_)" [6,6] 5)
- "@Rstar" :: "[sequence,sequence]=>prop" ("(_)|R>(_)" [6,6] 5)
- Lstar,Rstar :: "[sobj=>sobj,sobj=>sobj]=>prop"
+ box :: "o=>o" ("[]_" [50] 50)
+ dia :: "o=>o" ("<>_" [50] 50)
+ "--<",">-<" :: "[o,o]=>o" (infixr 25)
+ "@Lstar" :: "[sequence,sequence]=>prop" ("(_)|L>(_)" [6,6] 5)
+ "@Rstar" :: "[sequence,sequence]=>prop" ("(_)|R>(_)" [6,6] 5)
+ Lstar,Rstar :: "[sobj=>sobj,sobj=>sobj]=>prop"
rules
(* Definitions *)
- strimp_def "P --< Q == [](P --> Q)"
- streqv_def "P >-< Q == (P --< Q) & (Q --< P)"
+ strimp_def "P --< Q == [](P --> Q)"
+ streqv_def "P >-< Q == (P --< Q) & (Q --< P)"
end
ML
--- a/src/Modal/S4.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/Modal/S4.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: 91/Modal/S4
+(* Title: 91/Modal/S4
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1991 University of Cambridge
*)
--- a/src/Modal/S43.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/Modal/S43.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: 91/Modal/S43
+(* Title: 91/Modal/S43
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1991 University of Cambridge
This implements Rajeev Gore's sequent calculus for S43.
@@ -9,10 +9,10 @@
S43 = Modal0 +
consts
- S43pi :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,
- sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
+ S43pi :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,
+ sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
"@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,
- sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
+ sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
rules
(* Definition of the star operation using a set of Horn clauses *)
@@ -69,9 +69,9 @@
val tr' = LK.seq_tr1';
fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
- Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
+ Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
fun s43pi_tr'[Abs(_,_,s1),Abs(_,_,s2),Abs(_,_,s3),
- Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] =
+ Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] =
Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
in
val parse_translation = [(SS43pi,s43pi_tr)];
--- a/src/Modal/T.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/Modal/T.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: 91/Modal/T
+(* Title: 91/Modal/T
ID: $Id$
- Author: Martin Coen
+ Author: Martin Coen
Copyright 1991 University of Cambridge
*)