--- a/src/CTT/CTT.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/CTT/CTT.thy Wed Apr 14 14:13:05 2004 +0200
@@ -73,6 +73,14 @@
"@PROD" :: "[idt,t,t] => t" ("(3\\<Pi> _\\<in>_./ _)" 10)
"lam " :: "[idts, i] => i" ("(3\\<lambda>\\<lambda>_./ _)" 10)
+syntax (HTML output)
+ "@*" :: "[t,t]=>t" ("(_ \\<times>/ _)" [51,50] 50)
+ Elem :: "[i, t]=>prop" ("(_ /\\<in> _)" [10,10] 5)
+ Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
+ "@SUM" :: "[idt,t,t] => t" ("(3\\<Sigma> _\\<in>_./ _)" 10)
+ "@PROD" :: "[idt,t,t] => t" ("(3\\<Pi> _\\<in>_./ _)" 10)
+ "lam " :: "[idts, i] => i" ("(3\\<lambda>\\<lambda>_./ _)" 10)
+
rules
(*Reduction: a weaker notion than equality; a hack for simplification.
--- a/src/FOL/IFOL.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/FOL/IFOL.thy Wed Apr 14 14:13:05 2004 +0200
@@ -60,6 +60,12 @@
syntax (HTML output)
Not :: "o => o" ("\<not> _" [40] 40)
+ "op &" :: "[o, o] => o" (infixr "\<and>" 35)
+ "op |" :: "[o, o] => o" (infixr "\<or>" 30)
+ "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
+ "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
+ "_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50)
local
--- a/src/HOL/Finite_Set.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Finite_Set.thy Wed Apr 14 14:13:05 2004 +0200
@@ -746,6 +746,8 @@
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_:_. _" [0, 51, 10] 10)
syntax (xsymbols)
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
+syntax (HTML output)
+ "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
translations
"\<Sum>i:A. b" == "setsum (%i. b) A" -- {* Beware of argument permutation! *}
@@ -988,6 +990,9 @@
syntax (xsymbols)
"_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+syntax (HTML output)
+ "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+ ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
translations
"\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *}
--- a/src/HOL/Fun.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Fun.thy Wed Apr 14 14:13:05 2004 +0200
@@ -52,6 +52,8 @@
syntax (xsymbols)
comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55)
+syntax (HTML output)
+ comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55)
constdefs
--- a/src/HOL/HOL.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/HOL.thy Wed Apr 14 14:13:05 2004 +0200
@@ -102,7 +102,14 @@
"_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
syntax (HTML output)
+ "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
Not :: "bool => bool" ("\<not> _" [40] 40)
+ "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35)
+ "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30)
+ "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
+ "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10)
+ "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10)
syntax (HOL)
"ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10)
@@ -639,6 +646,10 @@
"op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
+syntax (HTML output)
+ "op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
+ "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
+
lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
by blast
@@ -1056,6 +1067,12 @@
"_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
"_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
+syntax (HTML output)
+ "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
+ "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
+ "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
+ "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+
translations
"ALL x<y. P" => "ALL x. x < y --> P"
"EX x<y. P" => "EX x. x < y & P"
--- a/src/HOL/Hyperreal/HyperDef.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Wed Apr 14 14:13:05 2004 +0200
@@ -68,6 +68,10 @@
omega :: hypreal ("\<omega>")
epsilon :: hypreal ("\<epsilon>")
+syntax (HTML output)
+ omega :: hypreal ("\<omega>")
+ epsilon :: hypreal ("\<epsilon>")
+
defs (overloaded)
--- a/src/HOL/Hyperreal/IntFloor.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Hyperreal/IntFloor.thy Wed Apr 14 14:13:05 2004 +0200
@@ -20,6 +20,9 @@
floor :: "real => int" ("\<lfloor>_\<rfloor>")
ceiling :: "real => int" ("\<lceil>_\<rceil>")
+syntax (HTML output)
+ floor :: "real => int" ("\<lfloor>_\<rfloor>")
+ ceiling :: "real => int" ("\<lceil>_\<rceil>")
lemma number_of_less_real_of_int_iff [simp]:
--- a/src/HOL/Hyperreal/NSA.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Apr 14 14:13:05 2004 +0200
@@ -43,6 +43,9 @@
syntax (xsymbols)
approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
+syntax (HTML output)
+ approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50)
+
subsection{*Closure Laws for Standard Reals*}
--- a/src/HOL/IMP/Compiler0.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Compiler0.thy Wed Apr 14 14:13:05 2004 +0200
@@ -39,6 +39,14 @@
"_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
+syntax (HTML output)
+ "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
+ "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+ ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
+ "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
+ ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
+
translations
"P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
"P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
--- a/src/HOL/IMP/Machines.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Machines.thy Wed Apr 14 14:13:05 2004 +0200
@@ -50,6 +50,14 @@
"_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+syntax (HTML output)
+ "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+ ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+ "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+ ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+ "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
+ ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+
translations
"p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
"p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
--- a/src/HOL/IMP/Natural.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Natural.thy Wed Apr 14 14:13:05 2004 +0200
@@ -17,6 +17,9 @@
syntax (xsymbols)
"_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
+syntax (HTML output)
+ "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
+
text {*
We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
in state @{text s}, terminates in state @{text s'}}. Formally,
--- a/src/HOL/IMP/Transition.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Transition.thy Wed Apr 14 14:13:05 2004 +0200
@@ -35,6 +35,10 @@
"_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
"_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+syntax (HTML output)
+ "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
+ "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+
translations
"\<langle>c,s\<rangle>" == "(Some c, s)"
"\<langle>s\<rangle>" == "(None, s)"
--- a/src/HOL/Induct/QuoDataType.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Wed Apr 14 14:13:05 2004 +0200
@@ -26,6 +26,8 @@
"_msgrel" :: "[freemsg, freemsg] => bool" (infixl "~~" 50)
syntax (xsymbols)
"_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
+syntax (HTML output)
+ "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
translations
"X \<sim> Y" == "(X,Y) \<in> msgrel"
--- a/src/HOL/Infinite_Set.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Infinite_Set.thy Wed Apr 14 14:13:05 2004 +0200
@@ -359,6 +359,10 @@
"MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
"INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
+syntax (HTML output)
+ "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
+ "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
+
lemma INF_EX:
"(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
proof (unfold INF_def, rule ccontr)
--- a/src/HOL/Lambda/Type.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Lambda/Type.thy Wed Apr 14 14:13:05 2004 +0200
@@ -16,6 +16,8 @@
"e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
syntax (xsymbols)
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+syntax (HTML output)
+ shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
by (simp add: shift_def)
--- a/src/HOL/Library/FuncSet.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Library/FuncSet.thy Wed Apr 14 14:13:05 2004 +0200
@@ -30,6 +30,10 @@
funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60)
"@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+syntax (HTML output)
+ "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
+ "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+
translations
"PI x:A. B" => "Pi A (%x. B)"
"A -> B" => "Pi A (_K B)"
--- a/src/HOL/Library/Nat_Infinity.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Wed Apr 14 14:13:05 2004 +0200
@@ -30,6 +30,9 @@
syntax (xsymbols)
Infty :: inat ("\<infinity>")
+syntax (HTML output)
+ Infty :: inat ("\<infinity>")
+
defs
Zero_inat_def: "0 == Fin 0"
iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>"
--- a/src/HOL/Library/Word.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Library/Word.thy Wed Apr 14 14:13:05 2004 +0200
@@ -260,6 +260,12 @@
bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+syntax (HTML output)
+ bitnot :: "bit => bit" ("\<not>\<^sub>b _" [40] 40)
+ bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
+ bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
+ bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+
primrec
bitnot_zero: "(bitnot \<zero>) = \<one>"
bitnot_one : "(bitnot \<one>) = \<zero>"
--- a/src/HOL/List.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/List.thy Wed Apr 14 14:13:05 2004 +0200
@@ -71,6 +71,8 @@
syntax (xsymbols)
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
+syntax (HTML output)
+ "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
text {*
--- a/src/HOL/NanoJava/Equivalence.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Apr 14 14:13:05 2004 +0200
@@ -166,6 +166,8 @@
"MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
syntax (xsymbols)
MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
+syntax (HTML output)
+ MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
lemma MGF_implies_complete:
"\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
--- a/src/HOL/Product_Type.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Product_Type.thy Wed Apr 14 14:13:05 2004 +0200
@@ -159,6 +159,10 @@
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
+syntax (HTML output)
+ "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
+
print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Wed Apr 14 14:13:05 2004 +0200
@@ -20,6 +20,8 @@
syntax (xsymbols)
prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
+syntax (HTML output)
+ prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
subsection {* Vector space laws *}
--- a/src/HOL/Set.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Set.thy Wed Apr 14 14:13:05 2004 +0200
@@ -108,6 +108,20 @@
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+syntax (HTML output)
+ "_setle" :: "'a set => 'a set => bool" ("op \<subseteq>")
+ "_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50)
+ "_setless" :: "'a set => 'a set => bool" ("op \<subset>")
+ "_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50)
+ "op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70)
+ "op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65)
+ "op :" :: "'a => 'a set => bool" ("op \<in>")
+ "op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50)
+ "op ~:" :: "'a => 'a set => bool" ("op \<notin>")
+ "op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50)
+ "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
+ "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+
syntax (input)
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10)
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10)
@@ -120,6 +134,7 @@
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
+
translations
"op \<subseteq>" => "op <= :: _ set => _ set => bool"
"op \<subset>" => "op < :: _ set => _ set => bool"
--- a/src/HOL/TLA/Intensional.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/TLA/Intensional.thy Wed Apr 14 14:13:05 2004 +0200
@@ -162,7 +162,16 @@
"_liftNotMem" :: [lift, lift] => lift ("(_/ \\<notin> _)" [50, 51] 50)
syntax (HTML output)
+ "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50)
"_liftNot" :: lift => lift ("\\<not> _" [40] 40)
+ "_liftAnd" :: [lift, lift] => lift (infixr "\\<and>" 35)
+ "_liftOr" :: [lift, lift] => lift (infixr "\\<or>" 30)
+ "_RAll" :: [idts, lift] => lift ("(3\\<forall>_./ _)" [0, 10] 10)
+ "_REx" :: [idts, lift] => lift ("(3\\<exists>_./ _)" [0, 10] 10)
+ "_REx1" :: [idts, lift] => lift ("(3\\<exists>!_./ _)" [0, 10] 10)
+ "_liftLeq" :: [lift, lift] => lift ("(_/ \\<le> _)" [50, 51] 50)
+ "_liftMem" :: [lift, lift] => lift ("(_/ \\<in> _)" [50, 51] 50)
+ "_liftNotMem" :: [lift, lift] => lift ("(_/ \\<notin> _)" [50, 51] 50)
rules
Valid_def "|- A == ALL w. w |= A"
--- a/src/HOL/TLA/TLA.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/TLA/TLA.thy Wed Apr 14 14:13:05 2004 +0200
@@ -62,6 +62,10 @@
"_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
"_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
+syntax (HTML output)
+ "_EEx" :: [idts, lift] => lift ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
+ "_AAll" :: [idts, lift] => lift ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
+
rules
(* Definitions of derived operators *)
dmd_def "TEMP <>F == TEMP ~[]~F"
--- a/src/HOL/Transitive_Closure.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Transitive_Closure.thy Wed Apr 14 14:13:05 2004 +0200
@@ -43,6 +43,11 @@
trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
"_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
+syntax (HTML output)
+ rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999)
+ trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
+ "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
+
subsection {* Reflexive-transitive closure *}
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Apr 14 14:13:05 2004 +0200
@@ -42,6 +42,8 @@
syntax (HTML output)
"NOT" ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
+ "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<and>" 35)
+ "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\\<or>" 30)
defs
--- a/src/HOLCF/Sprod0.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOLCF/Sprod0.thy Wed Apr 14 14:13:05 2004 +0200
@@ -16,6 +16,8 @@
syntax (xsymbols)
"**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
+syntax (HTML output)
+ "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
consts
Ispair :: "['a,'b] => ('a ** 'b)"
--- a/src/HOLCF/Ssum0.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOLCF/Ssum0.thy Wed Apr 14 14:13:05 2004 +0200
@@ -19,6 +19,8 @@
syntax (xsymbols)
"++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
+syntax (HTML output)
+ "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
consts
Isinl :: "'a => ('a ++ 'b)"
--- a/src/Pure/Thy/html.ML Wed Apr 14 13:28:46 2004 +0200
+++ b/src/Pure/Thy/html.ML Wed Apr 14 14:13:05 2004 +0200
@@ -156,8 +156,8 @@
| "\\<nabla>" => (1.0, "∇")
| "\\<in>" => (1.0, "∈")
| "\\<notin>" => (1.0, "∉")
- | "\\<prod>" => (1.0, "∏")
- | "\\<sum>" => (1.0, "∑")
+ | "\\<Prod>" => (1.0, "∏")
+ | "\\<Sum>" => (1.0, "∑")
| "\\<star>" => (1.0, "∗")
| "\\<propto>" => (1.0, "∝")
| "\\<infinity>" => (1.0, "∞")
--- a/src/Sequents/LK0.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/Sequents/LK0.thy Wed Apr 14 14:13:05 2004 +0200
@@ -53,6 +53,12 @@
syntax (HTML output)
Not :: o => o ("\\<not> _" [40] 40)
+ "op &" :: [o, o] => o (infixr "\\<and>" 35)
+ "op |" :: [o, o] => o (infixr "\\<or>" 30)
+ "ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10)
+ "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10)
+ "_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50)
local
--- a/src/ZF/Cardinal.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Cardinal.thy Wed Apr 14 14:13:05 2004 +0200
@@ -39,6 +39,10 @@
"lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50)
"LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
+syntax (HTML output)
+ "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
+ "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
+
subsection{*The Schroeder-Bernstein Theorem*}
text{*See Davey and Priestly, page 106*}
--- a/src/ZF/CardinalArith.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/CardinalArith.thy Wed Apr 14 14:13:05 2004 +0200
@@ -39,6 +39,9 @@
syntax (xsymbols)
"op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65)
"op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70)
+syntax (HTML output)
+ "op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65)
+ "op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70)
lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
--- a/src/ZF/Integ/Int.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Integ/Int.thy Wed Apr 14 14:13:05 2004 +0200
@@ -82,6 +82,7 @@
syntax (HTML output)
zmult :: "[i,i]=>i" (infixl "$\<times>" 70)
+ zle :: "[i,i]=>o" (infixl "$\<le>" 50)
declare quotientE [elim!]
--- a/src/ZF/Main.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Main.thy Wed Apr 14 14:13:05 2004 +0200
@@ -21,6 +21,8 @@
syntax (xsymbols)
iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60)
+syntax (HTML output)
+ iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60)
lemma iterates_triv:
"[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"
--- a/src/ZF/OrdQuant.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/OrdQuant.thy Wed Apr 14 14:13:05 2004 +0200
@@ -36,6 +36,10 @@
"@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
"@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
"@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
+syntax (HTML output)
+ "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
+ "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
+ "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
subsubsection {*simplification of the new quantifiers*}
@@ -204,6 +208,9 @@
syntax (xsymbols)
"@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
"@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
+syntax (HTML output)
+ "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
+ "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
translations
"ALL x[M]. P" == "rall(M, %x. P)"
--- a/src/ZF/Ordinal.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Ordinal.thy Wed Apr 14 14:13:05 2004 +0200
@@ -34,6 +34,8 @@
syntax (xsymbols)
"op le" :: "[i,i] => o" (infixl "\<le>" 50) (*less-than or equals*)
+syntax (HTML output)
+ "op le" :: "[i,i] => o" (infixl "\<le>" 50) (*less-than or equals*)
subsection{*Rules for Transset*}
--- a/src/ZF/ZF.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/ZF.thy Wed Apr 14 14:13:05 2004 +0200
@@ -170,6 +170,25 @@
syntax (HTML output)
"op *" :: "[i, i] => i" (infixr "\<times>" 80)
+ "op Int" :: "[i, i] => i" (infixl "\<inter>" 70)
+ "op Un" :: "[i, i] => i" (infixl "\<union>" 65)
+ "op <=" :: "[i, i] => o" (infixl "\<subseteq>" 50)
+ "op :" :: "[i, i] => o" (infixl "\<in>" 50)
+ "op ~:" :: "[i, i] => o" (infixl "\<notin>" 50)
+ "@Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})")
+ "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+ "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
+ "@UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
+ "@INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
+ Union :: "i =>i" ("\<Union>_" [90] 90)
+ Inter :: "i =>i" ("\<Inter>_" [90] 90)
+ "@PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10)
+ "@SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10)
+ "@lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
+ "@Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
+ "@Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
+ "@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
+ "@pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
finalconsts