--- a/src/CCL/Term.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/CCL/Term.thy Fri May 21 21:14:18 2004 +0200
@@ -37,6 +37,7 @@
letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
+syntax
"@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)"
[0,0,60] 60)
@@ -49,6 +50,7 @@
"@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
[0,0,0,0,0,60] 60)
+consts
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
rules
--- a/src/CCL/Type.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/CCL/Type.thy Fri May 21 21:14:18 2004 +0200
@@ -27,6 +27,7 @@
SPLIT :: "[i, [i, i] => i set] => i set"
+syntax
"@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)"
[0,0,60] 60)
--- a/src/CTT/CTT.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/CTT/CTT.thy Fri May 21 21:14:18 2004 +0200
@@ -34,6 +34,8 @@
split :: "[i, [i,i]=>i] =>i"
(*General Product and Function Space*)
Prod :: "[t, i=>t]=>t"
+ (*Types*)
+ "+" :: "[t,t]=>t" (infixr 40)
(*Equality type*)
Eq :: "[t,i,i]=>t"
eq :: "i"
@@ -44,12 +46,7 @@
Eqelem :: "[i,i,t]=>prop" ("(_ =/ _ :/ _)" [10,10,10] 5)
Reduce :: "[i,i]=>prop" ("Reduce[_,_]")
(*Types*)
- "@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
- "@SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
- "+" :: "[t,t]=>t" (infixr 40)
- (*Invisible infixes!*)
- "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30)
- "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50)
+
(*Functions*)
lambda :: "(i => i) => i" (binder "lam " 10)
"`" :: "[i,i]=>i" (infixl 60)
@@ -58,6 +55,12 @@
(*Pairing*)
pair :: "[i,i]=>i" ("(1<_,/_>)")
+syntax
+ "@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
+ "@SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
+ "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30)
+ "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50)
+
translations
"PROD x:A. B" => "Prod(A, %x. B)"
"A --> B" => "Prod(A, _K(B))"
--- a/src/HOL/Induct/SList.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/HOL/Induct/SList.thy Fri May 21 21:14:18 2004 +0200
@@ -90,6 +90,7 @@
(* list Enumeration *)
consts
"[]" :: "'a list" ("[]")
+syntax
"@list" :: "args => 'a list" ("[(_)]")
translations
--- a/src/Sequents/ILL.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/Sequents/ILL.thy Fri May 21 21:14:18 2004 +0200
@@ -8,12 +8,7 @@
ILL = Sequents +
consts
-
-
- Trueprop :: "two_seqi"
- "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
-
-
+ Trueprop :: "two_seqi"
"><" ::"[o, o] => o" (infixr 35)
"-o" ::"[o, o] => o" (infixr 45)
@@ -27,15 +22,18 @@
aneg ::"o=>o" ("~_")
- (* syntax for context manipulation *)
+ (* context manipulation *)
Context :: "two_seqi"
-"@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
- (* syntax for promotion rule *)
+ (* promotion rule *)
PromAux :: "three_seqi"
-"@PromAux":: "three_seqe" ("promaux {_||_||_}")
+
+syntax
+ "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
+ "@PromAux" :: "three_seqe" ("promaux {_||_||_}")
defs
@@ -47,7 +45,7 @@
rules
-
+
identity "P |- P"
zerol "$G, 0, $H |- A"
@@ -58,7 +56,7 @@
(* unfortunately, this one removes !A *)
contract "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
-
+
weaken "$F, $G |- C ==> $G, !A, $F |- C"
(* weak form of weakening, in practice just to clean context *)
(* weaken and contract not needed (CHECK) *)
@@ -69,7 +67,7 @@
promote0 "$G |- A ==> promaux {$G || || A}"
-
+
tensl "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
impr "A, $F |- B ==> $F |- A -o B"
@@ -101,7 +99,7 @@
$G |- A |]
==> $J, A -o B, $H |- C"
-
+
cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
$H1, $H2, $H3, $H4 |- A ;
$J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B"
@@ -118,7 +116,7 @@
-
+
end
ML
@@ -131,4 +129,4 @@
("Context",Sequents.two_seq_tr'"@Context"),
("PromAux", Sequents.three_seq_tr'"@PromAux")];
-
+
--- a/src/Sequents/LK0.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/Sequents/LK0.thy Fri May 21 21:14:18 2004 +0200
@@ -22,7 +22,6 @@
consts
Trueprop :: "two_seqi"
- "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
True,False :: o
"=" :: ['a,'a] => o (infixl 50)
@@ -35,6 +34,7 @@
Ex :: ('a => o) => o (binder "EX " 10)
syntax
+ "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
"_not_equal" :: ['a, 'a] => o (infixl "~=" 50)
translations
--- a/src/Sequents/Modal0.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/Sequents/Modal0.thy Fri May 21 21:14:18 2004 +0200
@@ -10,9 +10,11 @@
box :: "o=>o" ("[]_" [50] 50)
dia :: "o=>o" ("<>_" [50] 50)
"--<",">-<" :: "[o,o]=>o" (infixr 25)
+ Lstar,Rstar :: "two_seqi"
+
+syntax
"@Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5)
"@Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5)
- Lstar,Rstar :: "two_seqi"
rules
(* Definitions *)
--- a/src/Sequents/S43.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/Sequents/S43.thy Fri May 21 21:14:18 2004 +0200
@@ -11,6 +11,7 @@
consts
S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+syntax
"@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
--- a/src/Sequents/Sequents.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/Sequents/Sequents.thy Fri May 21 21:14:18 2004 +0200
@@ -30,7 +30,7 @@
(* concrete syntax *)
-types
+nonterminals
seq seqobj seqcont
@@ -59,7 +59,7 @@
sequence_name = seq'=>seq'
-consts
+syntax
(*Constant to allow definitions of SEQUENCES of formulas*)
"@Side" :: seq=>(seq'=>seq') ("<<(_)>>")