1.1 --- a/src/CTT/CTT.thy Wed Apr 14 13:28:46 2004 +0200
1.2 +++ b/src/CTT/CTT.thy Wed Apr 14 14:13:05 2004 +0200
1.3 @@ -73,6 +73,14 @@
1.4 "@PROD" :: "[idt,t,t] => t" ("(3\\<Pi> _\\<in>_./ _)" 10)
1.5 "lam " :: "[idts, i] => i" ("(3\\<lambda>\\<lambda>_./ _)" 10)
1.6
1.7 +syntax (HTML output)
1.8 + "@*" :: "[t,t]=>t" ("(_ \\<times>/ _)" [51,50] 50)
1.9 + Elem :: "[i, t]=>prop" ("(_ /\\<in> _)" [10,10] 5)
1.10 + Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
1.11 + "@SUM" :: "[idt,t,t] => t" ("(3\\<Sigma> _\\<in>_./ _)" 10)
1.12 + "@PROD" :: "[idt,t,t] => t" ("(3\\<Pi> _\\<in>_./ _)" 10)
1.13 + "lam " :: "[idts, i] => i" ("(3\\<lambda>\\<lambda>_./ _)" 10)
1.14 +
1.15 rules
1.16
1.17 (*Reduction: a weaker notion than equality; a hack for simplification.
2.1 --- a/src/FOL/IFOL.thy Wed Apr 14 13:28:46 2004 +0200
2.2 +++ b/src/FOL/IFOL.thy Wed Apr 14 14:13:05 2004 +0200
2.3 @@ -60,6 +60,12 @@
2.4
2.5 syntax (HTML output)
2.6 Not :: "o => o" ("\<not> _" [40] 40)
2.7 + "op &" :: "[o, o] => o" (infixr "\<and>" 35)
2.8 + "op |" :: "[o, o] => o" (infixr "\<or>" 30)
2.9 + "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
2.10 + "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
2.11 + "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
2.12 + "_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50)
2.13
2.14
2.15 local
3.1 --- a/src/HOL/Finite_Set.thy Wed Apr 14 13:28:46 2004 +0200
3.2 +++ b/src/HOL/Finite_Set.thy Wed Apr 14 14:13:05 2004 +0200
3.3 @@ -746,6 +746,8 @@
3.4 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_:_. _" [0, 51, 10] 10)
3.5 syntax (xsymbols)
3.6 "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
3.7 +syntax (HTML output)
3.8 + "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
3.9 translations
3.10 "\<Sum>i:A. b" == "setsum (%i. b) A" -- {* Beware of argument permutation! *}
3.11
3.12 @@ -988,6 +990,9 @@
3.13 syntax (xsymbols)
3.14 "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
3.15 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
3.16 +syntax (HTML output)
3.17 + "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
3.18 + ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
3.19 translations
3.20 "\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *}
3.21
4.1 --- a/src/HOL/Fun.thy Wed Apr 14 13:28:46 2004 +0200
4.2 +++ b/src/HOL/Fun.thy Wed Apr 14 14:13:05 2004 +0200
4.3 @@ -52,6 +52,8 @@
4.4
4.5 syntax (xsymbols)
4.6 comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55)
4.7 +syntax (HTML output)
4.8 + comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55)
4.9
4.10
4.11 constdefs
5.1 --- a/src/HOL/HOL.thy Wed Apr 14 13:28:46 2004 +0200
5.2 +++ b/src/HOL/HOL.thy Wed Apr 14 14:13:05 2004 +0200
5.3 @@ -102,7 +102,14 @@
5.4 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
5.5
5.6 syntax (HTML output)
5.7 + "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
5.8 Not :: "bool => bool" ("\<not> _" [40] 40)
5.9 + "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35)
5.10 + "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30)
5.11 + "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
5.12 + "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10)
5.13 + "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10)
5.14 + "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10)
5.15
5.16 syntax (HOL)
5.17 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10)
5.18 @@ -639,6 +646,10 @@
5.19 "op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
5.20 "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
5.21
5.22 +syntax (HTML output)
5.23 + "op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
5.24 + "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
5.25 +
5.26
5.27 lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
5.28 by blast
5.29 @@ -1056,6 +1067,12 @@
5.30 "_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
5.31 "_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
5.32
5.33 +syntax (HTML output)
5.34 + "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
5.35 + "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
5.36 + "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
5.37 + "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
5.38 +
5.39 translations
5.40 "ALL x<y. P" => "ALL x. x < y --> P"
5.41 "EX x<y. P" => "EX x. x < y & P"
6.1 --- a/src/HOL/Hyperreal/HyperDef.thy Wed Apr 14 13:28:46 2004 +0200
6.2 +++ b/src/HOL/Hyperreal/HyperDef.thy Wed Apr 14 14:13:05 2004 +0200
6.3 @@ -68,6 +68,10 @@
6.4 omega :: hypreal ("\<omega>")
6.5 epsilon :: hypreal ("\<epsilon>")
6.6
6.7 +syntax (HTML output)
6.8 + omega :: hypreal ("\<omega>")
6.9 + epsilon :: hypreal ("\<epsilon>")
6.10 +
6.11
6.12 defs (overloaded)
6.13
7.1 --- a/src/HOL/Hyperreal/IntFloor.thy Wed Apr 14 13:28:46 2004 +0200
7.2 +++ b/src/HOL/Hyperreal/IntFloor.thy Wed Apr 14 14:13:05 2004 +0200
7.3 @@ -20,6 +20,9 @@
7.4 floor :: "real => int" ("\<lfloor>_\<rfloor>")
7.5 ceiling :: "real => int" ("\<lceil>_\<rceil>")
7.6
7.7 +syntax (HTML output)
7.8 + floor :: "real => int" ("\<lfloor>_\<rfloor>")
7.9 + ceiling :: "real => int" ("\<lceil>_\<rceil>")
7.10
7.11
7.12 lemma number_of_less_real_of_int_iff [simp]:
8.1 --- a/src/HOL/Hyperreal/NSA.thy Wed Apr 14 13:28:46 2004 +0200
8.2 +++ b/src/HOL/Hyperreal/NSA.thy Wed Apr 14 14:13:05 2004 +0200
8.3 @@ -43,6 +43,9 @@
8.4 syntax (xsymbols)
8.5 approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
8.6
8.7 +syntax (HTML output)
8.8 + approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
8.9 +
8.10
8.11
8.12 subsection{*Closure Laws for Standard Reals*}
9.1 --- a/src/HOL/IMP/Compiler0.thy Wed Apr 14 13:28:46 2004 +0200
9.2 +++ b/src/HOL/IMP/Compiler0.thy Wed Apr 14 14:13:05 2004 +0200
9.3 @@ -39,6 +39,14 @@
9.4 "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
9.5 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
9.6
9.7 +syntax (HTML output)
9.8 + "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
9.9 + ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
9.10 + "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
9.11 + ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
9.12 + "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
9.13 + ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
9.14 +
9.15 translations
9.16 "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
9.17 "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
10.1 --- a/src/HOL/IMP/Machines.thy Wed Apr 14 13:28:46 2004 +0200
10.2 +++ b/src/HOL/IMP/Machines.thy Wed Apr 14 14:13:05 2004 +0200
10.3 @@ -50,6 +50,14 @@
10.4 "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
10.5 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
10.6
10.7 +syntax (HTML output)
10.8 + "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
10.9 + ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
10.10 + "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
10.11 + ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
10.12 + "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
10.13 + ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
10.14 +
10.15 translations
10.16 "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
10.17 "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
11.1 --- a/src/HOL/IMP/Natural.thy Wed Apr 14 13:28:46 2004 +0200
11.2 +++ b/src/HOL/IMP/Natural.thy Wed Apr 14 14:13:05 2004 +0200
11.3 @@ -17,6 +17,9 @@
11.4 syntax (xsymbols)
11.5 "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
11.6
11.7 +syntax (HTML output)
11.8 + "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
11.9 +
11.10 text {*
11.11 We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
11.12 in state @{text s}, terminates in state @{text s'}}. Formally,
12.1 --- a/src/HOL/IMP/Transition.thy Wed Apr 14 13:28:46 2004 +0200
12.2 +++ b/src/HOL/IMP/Transition.thy Wed Apr 14 14:13:05 2004 +0200
12.3 @@ -35,6 +35,10 @@
12.4 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
12.5 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
12.6
12.7 +syntax (HTML output)
12.8 + "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
12.9 + "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
12.10 +
12.11 translations
12.12 "\<langle>c,s\<rangle>" == "(Some c, s)"
12.13 "\<langle>s\<rangle>" == "(None, s)"
13.1 --- a/src/HOL/Induct/QuoDataType.thy Wed Apr 14 13:28:46 2004 +0200
13.2 +++ b/src/HOL/Induct/QuoDataType.thy Wed Apr 14 14:13:05 2004 +0200
13.3 @@ -26,6 +26,8 @@
13.4 "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "~~" 50)
13.5 syntax (xsymbols)
13.6 "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
13.7 +syntax (HTML output)
13.8 + "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
13.9 translations
13.10 "X \<sim> Y" == "(X,Y) \<in> msgrel"
13.11
14.1 --- a/src/HOL/Infinite_Set.thy Wed Apr 14 13:28:46 2004 +0200
14.2 +++ b/src/HOL/Infinite_Set.thy Wed Apr 14 14:13:05 2004 +0200
14.3 @@ -359,6 +359,10 @@
14.4 "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
14.5 "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
14.6
14.7 +syntax (HTML output)
14.8 + "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
14.9 + "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
14.10 +
14.11 lemma INF_EX:
14.12 "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
14.13 proof (unfold INF_def, rule ccontr)
15.1 --- a/src/HOL/Lambda/Type.thy Wed Apr 14 13:28:46 2004 +0200
15.2 +++ b/src/HOL/Lambda/Type.thy Wed Apr 14 14:13:05 2004 +0200
15.3 @@ -16,6 +16,8 @@
15.4 "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
15.5 syntax (xsymbols)
15.6 shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
15.7 +syntax (HTML output)
15.8 + shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
15.9
15.10 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
15.11 by (simp add: shift_def)
16.1 --- a/src/HOL/Library/FuncSet.thy Wed Apr 14 13:28:46 2004 +0200
16.2 +++ b/src/HOL/Library/FuncSet.thy Wed Apr 14 14:13:05 2004 +0200
16.3 @@ -30,6 +30,10 @@
16.4 funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60)
16.5 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
16.6
16.7 +syntax (HTML output)
16.8 + "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
16.9 + "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
16.10 +
16.11 translations
16.12 "PI x:A. B" => "Pi A (%x. B)"
16.13 "A -> B" => "Pi A (_K B)"
17.1 --- a/src/HOL/Library/Nat_Infinity.thy Wed Apr 14 13:28:46 2004 +0200
17.2 +++ b/src/HOL/Library/Nat_Infinity.thy Wed Apr 14 14:13:05 2004 +0200
17.3 @@ -30,6 +30,9 @@
17.4 syntax (xsymbols)
17.5 Infty :: inat ("\<infinity>")
17.6
17.7 +syntax (HTML output)
17.8 + Infty :: inat ("\<infinity>")
17.9 +
17.10 defs
17.11 Zero_inat_def: "0 == Fin 0"
17.12 iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>"
18.1 --- a/src/HOL/Library/Word.thy Wed Apr 14 13:28:46 2004 +0200
18.2 +++ b/src/HOL/Library/Word.thy Wed Apr 14 14:13:05 2004 +0200
18.3 @@ -260,6 +260,12 @@
18.4 bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
18.5 bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
18.6
18.7 +syntax (HTML output)
18.8 + bitnot :: "bit => bit" ("\<not>\<^sub>b _" [40] 40)
18.9 + bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
18.10 + bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
18.11 + bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
18.12 +
18.13 primrec
18.14 bitnot_zero: "(bitnot \<zero>) = \<one>"
18.15 bitnot_one : "(bitnot \<one>) = \<zero>"
19.1 --- a/src/HOL/List.thy Wed Apr 14 13:28:46 2004 +0200
19.2 +++ b/src/HOL/List.thy Wed Apr 14 14:13:05 2004 +0200
19.3 @@ -71,6 +71,8 @@
19.4
19.5 syntax (xsymbols)
19.6 "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
19.7 +syntax (HTML output)
19.8 + "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
19.9
19.10
19.11 text {*
20.1 --- a/src/HOL/NanoJava/Equivalence.thy Wed Apr 14 13:28:46 2004 +0200
20.2 +++ b/src/HOL/NanoJava/Equivalence.thy Wed Apr 14 14:13:05 2004 +0200
20.3 @@ -166,6 +166,8 @@
20.4 "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
20.5 syntax (xsymbols)
20.6 MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
20.7 +syntax (HTML output)
20.8 + MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
20.9
20.10 lemma MGF_implies_complete:
20.11 "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
21.1 --- a/src/HOL/Product_Type.thy Wed Apr 14 13:28:46 2004 +0200
21.2 +++ b/src/HOL/Product_Type.thy Wed Apr 14 14:13:05 2004 +0200
21.3 @@ -159,6 +159,10 @@
21.4 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
21.5 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
21.6
21.7 +syntax (HTML output)
21.8 + "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
21.9 + "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
21.10 +
21.11 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
21.12
21.13
22.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Apr 14 13:28:46 2004 +0200
22.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Apr 14 14:13:05 2004 +0200
22.3 @@ -20,6 +20,8 @@
22.4
22.5 syntax (xsymbols)
22.6 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
22.7 +syntax (HTML output)
22.8 + prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
22.9
22.10
22.11 subsection {* Vector space laws *}
23.1 --- a/src/HOL/Set.thy Wed Apr 14 13:28:46 2004 +0200
23.2 +++ b/src/HOL/Set.thy Wed Apr 14 14:13:05 2004 +0200
23.3 @@ -108,6 +108,20 @@
23.4 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
23.5 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
23.6
23.7 +syntax (HTML output)
23.8 + "_setle" :: "'a set => 'a set => bool" ("op \<subseteq>")
23.9 + "_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50)
23.10 + "_setless" :: "'a set => 'a set => bool" ("op \<subset>")
23.11 + "_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50)
23.12 + "op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70)
23.13 + "op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65)
23.14 + "op :" :: "'a => 'a set => bool" ("op \<in>")
23.15 + "op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50)
23.16 + "op ~:" :: "'a => 'a set => bool" ("op \<notin>")
23.17 + "op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50)
23.18 + "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
23.19 + "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
23.20 +
23.21 syntax (input)
23.22 "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10)
23.23 "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10)
23.24 @@ -120,6 +134,7 @@
23.25 "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
23.26 "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
23.27
23.28 +
23.29 translations
23.30 "op \<subseteq>" => "op <= :: _ set => _ set => bool"
23.31 "op \<subset>" => "op < :: _ set => _ set => bool"
24.1 --- a/src/HOL/TLA/Intensional.thy Wed Apr 14 13:28:46 2004 +0200
24.2 +++ b/src/HOL/TLA/Intensional.thy Wed Apr 14 14:13:05 2004 +0200
24.3 @@ -162,7 +162,16 @@
24.4 "_liftNotMem" :: [lift, lift] => lift ("(_/ \\<notin> _)" [50, 51] 50)
24.5
24.6 syntax (HTML output)
24.7 + "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50)
24.8 "_liftNot" :: lift => lift ("\\<not> _" [40] 40)
24.9 + "_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35)
24.10 + "_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30)
24.11 + "_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10)
24.12 + "_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10)
24.13 + "_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10)
24.14 + "_liftLeq" :: [lift, lift] => lift ("(_/ \\<le> _)" [50, 51] 50)
24.15 + "_liftMem" :: [lift, lift] => lift ("(_/ \\<in> _)" [50, 51] 50)
24.16 + "_liftNotMem" :: [lift, lift] => lift ("(_/ \\<notin> _)" [50, 51] 50)
24.17
24.18 rules
24.19 Valid_def "|- A == ALL w. w |= A"
25.1 --- a/src/HOL/TLA/TLA.thy Wed Apr 14 13:28:46 2004 +0200
25.2 +++ b/src/HOL/TLA/TLA.thy Wed Apr 14 14:13:05 2004 +0200
25.3 @@ -62,6 +62,10 @@
25.4 "_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
25.5 "_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
25.6
25.7 +syntax (HTML output)
25.8 + "_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
25.9 + "_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
25.10 +
25.11 rules
25.12 (* Definitions of derived operators *)
25.13 dmd_def "TEMP <>F == TEMP ~[]~F"
26.1 --- a/src/HOL/Transitive_Closure.thy Wed Apr 14 13:28:46 2004 +0200
26.2 +++ b/src/HOL/Transitive_Closure.thy Wed Apr 14 14:13:05 2004 +0200
26.3 @@ -43,6 +43,11 @@
26.4 trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
26.5 "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
26.6
26.7 +syntax (HTML output)
26.8 + rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999)
26.9 + trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
26.10 + "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
26.11 +
26.12
26.13 subsection {* Reflexive-transitive closure *}
26.14
27.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Apr 14 13:28:46 2004 +0200
27.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Apr 14 14:13:05 2004 +0200
27.3 @@ -42,6 +42,8 @@
27.4
27.5 syntax (HTML output)
27.6 "NOT" ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
27.7 + "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<and>" 35)
27.8 + "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<or>" 30)
27.9
27.10
27.11 defs
28.1 --- a/src/HOLCF/Sprod0.thy Wed Apr 14 13:28:46 2004 +0200
28.2 +++ b/src/HOLCF/Sprod0.thy Wed Apr 14 14:13:05 2004 +0200
28.3 @@ -16,6 +16,8 @@
28.4
28.5 syntax (xsymbols)
28.6 "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
28.7 +syntax (HTML output)
28.8 + "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
28.9
28.10 consts
28.11 Ispair :: "['a,'b] => ('a ** 'b)"
29.1 --- a/src/HOLCF/Ssum0.thy Wed Apr 14 13:28:46 2004 +0200
29.2 +++ b/src/HOLCF/Ssum0.thy Wed Apr 14 14:13:05 2004 +0200
29.3 @@ -19,6 +19,8 @@
29.4
29.5 syntax (xsymbols)
29.6 "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
29.7 +syntax (HTML output)
29.8 + "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
29.9
29.10 consts
29.11 Isinl :: "'a => ('a ++ 'b)"
30.1 --- a/src/Pure/Thy/html.ML Wed Apr 14 13:28:46 2004 +0200
30.2 +++ b/src/Pure/Thy/html.ML Wed Apr 14 14:13:05 2004 +0200
30.3 @@ -156,8 +156,8 @@
30.4 | "\\<nabla>" => (1.0, "∇")
30.5 | "\\<in>" => (1.0, "∈")
30.6 | "\\<notin>" => (1.0, "∉")
30.7 - | "\\<prod>" => (1.0, "∏")
30.8 - | "\\<sum>" => (1.0, "∑")
30.9 + | "\\<Prod>" => (1.0, "∏")
30.10 + | "\\<Sum>" => (1.0, "∑")
30.11 | "\\<star>" => (1.0, "∗")
30.12 | "\\<propto>" => (1.0, "∝")
30.13 | "\\<infinity>" => (1.0, "∞")
31.1 --- a/src/Sequents/LK0.thy Wed Apr 14 13:28:46 2004 +0200
31.2 +++ b/src/Sequents/LK0.thy Wed Apr 14 14:13:05 2004 +0200
31.3 @@ -53,6 +53,12 @@
31.4
31.5 syntax (HTML output)
31.6 Not :: o => o ("\\<not> _" [40] 40)
31.7 + "op &" :: [o, o] => o (infixr "\\<and>" 35)
31.8 + "op |" :: [o, o] => o (infixr "\\<or>" 30)
31.9 + "ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10)
31.10 + "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10)
31.11 + "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10)
31.12 + "_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50)
31.13
31.14
31.15 local
32.1 --- a/src/ZF/Cardinal.thy Wed Apr 14 13:28:46 2004 +0200
32.2 +++ b/src/ZF/Cardinal.thy Wed Apr 14 14:13:05 2004 +0200
32.3 @@ -39,6 +39,10 @@
32.4 "lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50)
32.5 "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
32.6
32.7 +syntax (HTML output)
32.8 + "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
32.9 + "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
32.10 +
32.11 subsection{*The Schroeder-Bernstein Theorem*}
32.12 text{*See Davey and Priestly, page 106*}
32.13
33.1 --- a/src/ZF/CardinalArith.thy Wed Apr 14 13:28:46 2004 +0200
33.2 +++ b/src/ZF/CardinalArith.thy Wed Apr 14 14:13:05 2004 +0200
33.3 @@ -39,6 +39,9 @@
33.4 syntax (xsymbols)
33.5 "op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65)
33.6 "op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70)
33.7 +syntax (HTML output)
33.8 + "op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65)
33.9 + "op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70)
33.10
33.11
33.12 lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
34.1 --- a/src/ZF/Integ/Int.thy Wed Apr 14 13:28:46 2004 +0200
34.2 +++ b/src/ZF/Integ/Int.thy Wed Apr 14 14:13:05 2004 +0200
34.3 @@ -82,6 +82,7 @@
34.4
34.5 syntax (HTML output)
34.6 zmult :: "[i,i]=>i" (infixl "$\<times>" 70)
34.7 + zle :: "[i,i]=>o" (infixl "$\<le>" 50)
34.8
34.9
34.10 declare quotientE [elim!]
35.1 --- a/src/ZF/Main.thy Wed Apr 14 13:28:46 2004 +0200
35.2 +++ b/src/ZF/Main.thy Wed Apr 14 14:13:05 2004 +0200
35.3 @@ -21,6 +21,8 @@
35.4
35.5 syntax (xsymbols)
35.6 iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60)
35.7 +syntax (HTML output)
35.8 + iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60)
35.9
35.10 lemma iterates_triv:
35.11 "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"
36.1 --- a/src/ZF/OrdQuant.thy Wed Apr 14 13:28:46 2004 +0200
36.2 +++ b/src/ZF/OrdQuant.thy Wed Apr 14 14:13:05 2004 +0200
36.3 @@ -36,6 +36,10 @@
36.4 "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
36.5 "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
36.6 "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
36.7 +syntax (HTML output)
36.8 + "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
36.9 + "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
36.10 + "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
36.11
36.12
36.13 subsubsection {*simplification of the new quantifiers*}
36.14 @@ -204,6 +208,9 @@
36.15 syntax (xsymbols)
36.16 "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
36.17 "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
36.18 +syntax (HTML output)
36.19 + "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
36.20 + "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
36.21
36.22 translations
36.23 "ALL x[M]. P" == "rall(M, %x. P)"
37.1 --- a/src/ZF/Ordinal.thy Wed Apr 14 13:28:46 2004 +0200
37.2 +++ b/src/ZF/Ordinal.thy Wed Apr 14 14:13:05 2004 +0200
37.3 @@ -34,6 +34,8 @@
37.4
37.5 syntax (xsymbols)
37.6 "op le" :: "[i,i] => o" (infixl "\<le>" 50) (*less-than or equals*)
37.7 +syntax (HTML output)
37.8 + "op le" :: "[i,i] => o" (infixl "\<le>" 50) (*less-than or equals*)
37.9
37.10
37.11 subsection{*Rules for Transset*}
38.1 --- a/src/ZF/ZF.thy Wed Apr 14 13:28:46 2004 +0200
38.2 +++ b/src/ZF/ZF.thy Wed Apr 14 14:13:05 2004 +0200
38.3 @@ -170,6 +170,25 @@
38.4
38.5 syntax (HTML output)
38.6 "op *" :: "[i, i] => i" (infixr "\<times>" 80)
38.7 + "op Int" :: "[i, i] => i" (infixl "\<inter>" 70)
38.8 + "op Un" :: "[i, i] => i" (infixl "\<union>" 65)
38.9 + "op <=" :: "[i, i] => o" (infixl "\<subseteq>" 50)
38.10 + "op :" :: "[i, i] => o" (infixl "\<in>" 50)
38.11 + "op ~:" :: "[i, i] => o" (infixl "\<notin>" 50)
38.12 + "@Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})")
38.13 + "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
38.14 + "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
38.15 + "@UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
38.16 + "@INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
38.17 + Union :: "i =>i" ("\<Union>_" [90] 90)
38.18 + Inter :: "i =>i" ("\<Inter>_" [90] 90)
38.19 + "@PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10)
38.20 + "@SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10)
38.21 + "@lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
38.22 + "@Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
38.23 + "@Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
38.24 + "@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
38.25 + "@pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
38.26
38.27
38.28 finalconsts