modernized syntax declarations, and make them actually work with authentic syntax;
--- a/src/HOL/Algebra/Congruence.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/Algebra/Congruence.thy Wed Feb 24 22:09:50 2010 +0100
@@ -35,15 +35,17 @@
eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
"is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
-syntax
+abbreviation
not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
- not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
- set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
+ where "x .\<noteq>\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)"
-translations
- "x .\<noteq>\<index> y" == "~(x .=\<index> y)"
- "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
- "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
+abbreviation
+ not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
+ where "x .\<notin>\<^bsub>S\<^esub> A == ~(x .\<in>\<^bsub>S\<^esub> A)"
+
+abbreviation
+ set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
+ where "A {.\<noteq>}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)"
locale equivalence =
fixes S (structure)
--- a/src/HOL/Bali/Basis.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/Bali/Basis.thy Wed Feb 24 22:09:50 2010 +0100
@@ -222,12 +222,12 @@
section "quantifiers for option type"
syntax
- Oall :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10)
- Oex :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10)
+ "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10)
+ "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10)
syntax (symbols)
- Oall :: "[pttrn, 'a option, bool] => bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
- Oex :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
+ "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
+ "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
translations
"! x:A: P" == "! x:CONST Option.set A. P"
--- a/src/HOL/Bali/Table.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/Bali/Table.thy Wed Feb 24 22:09:50 2010 +0100
@@ -37,11 +37,9 @@
section "map of / table of"
-syntax
- table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
-
abbreviation
- "table_of \<equiv> map_of"
+ table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
+ where "table_of \<equiv> map_of"
translations
(type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
--- a/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Wed Feb 24 22:09:50 2010 +0100
@@ -60,9 +60,8 @@
("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
"|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q"
-syntax (xsymbols)
- Valid :: "'a bexp => 'a com => 'a bexp => bool"
- ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+notation (xsymbols)
+ Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
lemma ValidI [intro?]:
"(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
--- a/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Wed Feb 24 22:09:50 2010 +0100
@@ -66,9 +66,8 @@
| Some x \<Rightarrow> frs = []"
-syntax (xsymbols)
- correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
- ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
+notation (xsymbols)
+ correct_state ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
lemma sup_ty_opt_OK:
--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 24 22:09:50 2010 +0100
@@ -59,15 +59,11 @@
"sup_state_opt G == Opt.le (sup_state G)"
-syntax (xsymbols)
- sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=o _" [71,71] 70)
- sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=l _" [71,71] 70)
- sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=s _" [71,71] 70)
- sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=' _" [71,71] 70)
+notation (xsymbols)
+ sup_ty_opt ("_ \<turnstile> _ <=o _" [71,71] 70) and
+ sup_loc ("_ \<turnstile> _ <=l _" [71,71] 70) and
+ sup_state ("_ \<turnstile> _ <=s _" [71,71] 70) and
+ sup_state_opt ("_ \<turnstile> _ <=' _" [71,71] 70)
lemma JVM_states_unfold:
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Feb 24 22:09:50 2010 +0100
@@ -19,9 +19,8 @@
comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a"
"comb_nil a == ([], a)"
-syntax (xsymbols)
- "comb" :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
- (infixr "\<box>" 55)
+notation (xsymbols)
+ comb (infixr "\<box>" 55)
lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
by (simp add: comb_def comb_nil_def split_beta)
--- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Feb 24 22:09:50 2010 +0100
@@ -32,16 +32,19 @@
"lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
(*<*)
-syntax
- (* allow \<sub> instead of \<bsub>..\<esub> *)
- "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
- "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
- "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+(* allow \<sub> instead of \<bsub>..\<esub> *)
+
+abbreviation (input)
+ lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
+ where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
-translations
- "x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
- "x \<sqsubset>\<^sub>r y" => "x \<sqsubset>\<^bsub>r\<^esub> y"
- "x \<squnion>\<^sub>f y" => "x \<squnion>\<^bsub>f\<^esub> y"
+abbreviation (input)
+ lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
+ where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y"
+
+abbreviation (input)
+ plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+ where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
(*>*)
defs
--- a/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Wed Feb 24 22:09:50 2010 +0100
@@ -38,24 +38,13 @@
xconf (heap (store s)) (abrupt s)"
-syntax (xsymbols)
- hext :: "aheap => aheap => bool"
- ("_ \<le>| _" [51,51] 50)
-
- conf :: "'c prog => aheap => val => ty => bool"
- ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
-
- lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
- ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
-
- oconf :: "'c prog => aheap => obj => bool"
- ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
-
- hconf :: "'c prog => aheap => bool"
- ("_ \<turnstile>h _ \<surd>" [51,51] 50)
-
- conforms :: "state => java_mb env' => bool"
- ("_ ::\<preceq> _" [51,51] 50)
+notation (xsymbols)
+ hext ("_ \<le>| _" [51,51] 50) and
+ conf ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and
+ lconf ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and
+ oconf ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and
+ hconf ("_ \<turnstile>h _ \<surd>" [51,51] 50) and
+ conforms ("_ ::\<preceq> _" [51,51] 50)
section "hext"
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Wed Feb 24 22:09:50 2010 +0100
@@ -123,19 +123,15 @@
| Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
-consts
- "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
+constdefs
+ exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
("_ |- _ -jvmd-> _" [61,61,61]60)
+ "G |- s -jvmd-> t \<equiv>
+ (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
+ {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
-syntax (xsymbols)
- "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
- ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
-
-defs
- exec_all_d_def:
- "G \<turnstile> s -jvmd\<rightarrow> t \<equiv>
- (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
- {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
+notation (xsymbols)
+ exec_all_d ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
declare split_paired_All [simp del]
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Wed Feb 24 22:09:50 2010 +0100
@@ -32,9 +32,8 @@
"G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
-syntax (xsymbols)
- exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
+notation (xsymbols)
+ exec_all ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
text {*
The start configuration of the JVM: in the start heap, we call a
--- a/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Feb 24 22:09:50 2010 +0100
@@ -33,14 +33,14 @@
cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60)
"A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
-syntax (xsymbols)
- valid :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60)
- envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60)
- nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60)
- cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
-cenvalid :: "[triple set,etriple ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
+notation (xsymbols)
+ valid ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
+ evalid ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
+ nvalid ("\<Turnstile>_: _" [61,61] 60) and
+ envalid ("\<Turnstile>_:\<^sub>e _" [61,61] 60) and
+ nvalids ("|\<Turnstile>_: _" [61,61] 60) and
+ cnvalids ("_ |\<Turnstile>/ _" [61,61] 60) and
+ cenvalid ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
@@ -164,10 +164,10 @@
"MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n\<rightarrow> t)"
MGTe :: "expr => state => etriple"
"MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
-syntax (xsymbols)
- MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
-syntax (HTML output)
- MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
+notation (xsymbols)
+ MGTe ("MGT\<^sub>e")
+notation (HTML output)
+ MGTe ("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/NanoJava/State.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/NanoJava/State.thy Wed Feb 24 22:09:50 2010 +0100
@@ -84,9 +84,9 @@
lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
"lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)"
-syntax (xsymbols)
- hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000)
- lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
+notation (xsymbols)
+ hupd ("hupd'(_\<mapsto>_')" [10,10] 1000) and
+ lupd ("lupd'(_\<mapsto>_')" [10,10] 1000)
constdefs
--- a/src/HOL/UNITY/SubstAx.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Wed Feb 24 22:09:50 2010 +0100
@@ -17,8 +17,8 @@
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60)
"A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
-syntax (xsymbols)
- "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
+notation (xsymbols)
+ LeadsTo (infixl " \<longmapsto>w " 60)
text{*Resembles the previous definition of LeadsTo*}
--- a/src/HOL/UNITY/WFair.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/UNITY/WFair.thy Wed Feb 24 22:09:50 2010 +0100
@@ -69,8 +69,8 @@
--{*predicate transformer: the largest set that leads to @{term B}*}
"wlt F B == Union {A. F \<in> A leadsTo B}"
-syntax (xsymbols)
- "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
+notation (xsymbols)
+ leadsTo (infixl "\<longmapsto>" 60)
subsection{*transient*}
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Wed Feb 24 22:09:50 2010 +0100
@@ -24,25 +24,25 @@
IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr ".-->" 25)
-syntax ("" output)
- "NOT" ::"'a predicate => 'a predicate" ("~ _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "&" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "|" 30)
- "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "-->" 25)
+notation (output)
+ NOT ("~ _" [40] 40) and
+ AND (infixr "&" 35) and
+ OR (infixr "|" 30) and
+ IMPLIES (infixr "-->" 25)
-syntax (xsymbols 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)
- "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<longrightarrow>" 25)
+notation (xsymbols output)
+ NOT ("\<not> _" [40] 40) and
+ AND (infixr "\<and>" 35) and
+ OR (infixr "\<or>" 30) and
+ IMPLIES (infixr "\<longrightarrow>" 25)
-syntax (xsymbols)
- "satisfies" ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
+notation (xsymbols)
+ satisfies ("_ \<Turnstile> _" [100,9] 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)
+notation (HTML output)
+ NOT ("\<not> _" [40] 40) and
+ AND (infixr "\<and>" 35) and
+ OR (infixr "\<or>" 30)
defs
--- a/src/Sequents/LK0.thy Wed Feb 24 22:04:10 2010 +0100
+++ b/src/Sequents/LK0.thy Wed Feb 24 22:09:50 2010 +0100
@@ -43,23 +43,23 @@
not_equal (infixl "~=" 50) where
"x ~= y == ~ (x = y)"
-syntax (xsymbols)
- Not :: "o => o" ("\<not> _" [40] 40)
- conj :: "[o, o] => o" (infixr "\<and>" 35)
- disj :: "[o, o] => o" (infixr "\<or>" 30)
- imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
- iff :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
- All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+notation (xsymbols)
+ Not ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ imp (infixr "\<longrightarrow>" 25) and
+ iff (infixr "\<longleftrightarrow>" 25) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ not_equal (infixl "\<noteq>" 50)
-syntax (HTML output)
- Not :: "o => o" ("\<not> _" [40] 40)
- conj :: "[o, o] => o" (infixr "\<and>" 35)
- disj :: "[o, o] => o" (infixr "\<or>" 30)
- All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+notation (HTML output)
+ Not ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ not_equal (infixl "\<noteq>" 50)
local