--- a/src/CTT/CTT.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/CTT/CTT.thy Sun Nov 26 18:07:16 2006 +0100
@@ -72,25 +72,25 @@
"A * B == SUM _:A. B"
notation (xsymbols)
+ lambda (binder "\<lambda>\<lambda>" 10) and
Elem ("(_ /\<in> _)" [10,10] 5) and
Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
Arrow (infixr "\<longrightarrow>" 30) and
Times (infixr "\<times>" 50)
notation (HTML output)
+ lambda (binder "\<lambda>\<lambda>" 10) and
Elem ("(_ /\<in> _)" [10,10] 5) and
Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
Times (infixr "\<times>" 50)
syntax (xsymbols)
- "@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)
+ "_PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
+ "_SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
syntax (HTML output)
- "@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)
+ "_PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
+ "_SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
axioms
--- a/src/FOL/IFOL.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/FOL/IFOL.thy Sun Nov 26 18:07:16 2006 +0100
@@ -54,24 +54,23 @@
notation (HTML output)
not_equal (infixl "\<noteq>" 50)
-syntax (xsymbols)
- 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)
- "op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
- "op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
+notation (xsymbols)
+ Not ("\<not> _" [40] 40) and
+ "op &" (infixr "\<and>" 35) and
+ "op |" (infixr "\<or>" 30) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ Ex1 (binder "\<exists>!" 10) and
+ "op -->" (infixr "\<longrightarrow>" 25) and
+ "op <->" (infixr "\<longleftrightarrow>" 25)
-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)
-
+notation (HTML output)
+ Not ("\<not> _" [40] 40) and
+ "op &" (infixr "\<and>" 35) and
+ "op |" (infixr "\<or>" 30) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ Ex1 (binder "\<exists>!" 10)
local
--- a/src/HOL/HOL.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/HOL/HOL.thy Sun Nov 26 18:07:16 2006 +0100
@@ -115,21 +115,22 @@
*}
syntax (xsymbols)
- "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)
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
-(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \<orelse> _")*)
+
+notation (xsymbols)
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ Ex1 (binder "\<exists>!" 10)
-syntax (HTML output)
- "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)
+notation (HTML output)
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ Ex1 (binder "\<exists>!" 10)
-syntax (HOL)
- "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10)
- "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10)
- "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10)
+notation (HOL)
+ All (binder "! " 10) and
+ Ex (binder "? " 10) and
+ Ex1 (binder "?! " 10)
subsubsection {* Axioms and basic definitions *}
@@ -179,27 +180,35 @@
subsubsection {* Generic algebraic operations *}
class zero =
- fixes zero :: "'a" ("\<^loc>0")
+ fixes zero :: "'a" ("\<^loc>0")
class one =
- fixes one :: "'a" ("\<^loc>1")
+ fixes one :: "'a" ("\<^loc>1")
hide (open) const zero one
class plus =
- fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65)
+ fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>+" 65)
class minus =
fixes uminus :: "'a \<Rightarrow> 'a"
- fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>-" 65)
- fixes abs :: "'a \<Rightarrow> 'a"
+ and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>-" 65)
+ and abs :: "'a \<Rightarrow> 'a"
class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>*" 70)
class inverse =
fixes inverse :: "'a \<Rightarrow> 'a"
- fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70)
+ and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>'/" 70)
+
+notation
+ uminus ("- _" [81] 80)
+
+notation (xsymbols)
+ abs ("\<bar>_\<bar>")
+notation (HTML output)
+ abs ("\<bar>_\<bar>")
syntax
"_index1" :: index ("\<^sub>1")
@@ -215,14 +224,6 @@
in map (tr' o Sign.const_syntax_name thy) ["HOL.one", "HOL.zero"] end;
*} -- {* show types that are presumably too general *}
-notation
- uminus ("- _" [81] 80)
-
-notation (xsymbols)
- abs ("\<bar>_\<bar>")
-notation (HTML output)
- abs ("\<bar>_\<bar>")
-
subsection {* Fundamental rules *}
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Sun Nov 26 18:07:16 2006 +0100
@@ -16,8 +16,8 @@
"op &" :: "[bool, bool] => bool" (infixr "AND" 35)
"op |" :: "[bool, bool] => bool" (infixr "OR" 30)
- "ALL " :: "[idts, bool] => bool" ("'((3A _./ _)')" [0, 10] 10)
- "EX " :: "[idts, bool] => bool" ("'((3E _./ _)')" [0, 10] 10)
+ All_binder :: "[idts, bool] => bool" ("'((3A _./ _)')" [0, 10] 10)
+ Ex_binder :: "[idts, bool] => bool" ("'((3E _./ _)')" [0, 10] 10)
"_lambda" :: "[pttrns, 'a] => 'b" ("(3L _./ _)" 10)
"_idts" :: "[idt, idts] => idts" ("_,/_" [1, 0] 0)
--- a/src/HOL/Modelcheck/MuckeSyn.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Sun Nov 26 18:07:16 2006 +0100
@@ -29,8 +29,8 @@
"op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50)
"_not_equal" :: "['a, 'a] => bool" ("(_ !=/ _)" [51, 51] 50)
- "ALL " :: "[idts, bool] => bool" ("'((3forall _./ _)')" [0, 10] 10)
- "EX " :: "[idts, bool] => bool" ("'((3exists _./ _)')" [0, 10] 10)
+ All_binder :: "[idts, bool] => bool" ("'((3forall _./ _)')" [0, 10] 10)
+ Ex_binder :: "[idts, bool] => bool" ("'((3exists _./ _)')" [0, 10] 10)
"_lambda" :: "[idts, 'a] => 'b" ("(3L _./ _)" 10)
"_applC" :: "[('b => 'a), cargs] => aprop" ("(1_/ '(_'))" [1000,1000] 999)
--- a/src/HOL/Orderings.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/HOL/Orderings.thy Sun Nov 26 18:07:16 2006 +0100
@@ -547,16 +547,19 @@
print_translation {*
let
val syntax_name = Sign.const_syntax_name (the_context ());
+ val binder_name = Syntax.binder_name o syntax_name;
+ val All_binder = binder_name "All";
+ val Ex_binder = binder_name "Ex";
val impl = syntax_name "op -->";
val conj = syntax_name "op &";
val less = syntax_name "Orderings.less";
val less_eq = syntax_name "Orderings.less_eq";
val trans =
- [(("ALL ", impl, less), ("_All_less", "_All_greater")),
- (("ALL ", impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
- (("EX ", conj, less), ("_Ex_less", "_Ex_greater")),
- (("EX ", conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
+ [((All_binder, impl, less), ("_All_less", "_All_greater")),
+ ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
+ ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
+ ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
fun mk v v' c n P =
if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
@@ -572,7 +575,7 @@
| (n, Const ("_bound", _) $ Free (v', _)) => mk v v' g n P
| _ => raise Match))
| _ => raise Match);
-in [tr' "ALL ", tr' "EX "] end
+in [tr' All_binder, tr' Ex_binder] end
*}
--- a/src/HOL/Set.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/HOL/Set.thy Sun Nov 26 18:07:16 2006 +0100
@@ -249,7 +249,7 @@
then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
else raise Match)
in
-[("ALL ", all_tr'), ("EX ", ex_tr')]
+[("All_binder", all_tr'), ("Ex_binder", ex_tr')]
end
*}
--- a/src/HOLCF/Porder.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/HOLCF/Porder.thy Sun Nov 26 18:07:16 2006 +0100
@@ -87,14 +87,13 @@
lub :: "'a set \<Rightarrow> 'a::po"
"lub S \<equiv> THE x. S <<| x"
-syntax
- "@LUB" :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "LUB " 10)
+abbreviation
+ Lub (binder "LUB " 10) where
+ "LUB n. t n == lub (range t)"
-syntax (xsymbols)
- "LUB " :: "[idts, 'a] \<Rightarrow> 'a" ("(3\<Squnion>_./ _)" [0,10] 10)
+notation (xsymbols)
+ Lub (binder "\<Squnion> " 10)
-translations
- "\<Squnion>n. t" == "lub(CONST range(\<lambda>n. t))"
text {* lubs are unique *}
--- a/src/Pure/pure_thy.ML Fri Nov 24 22:05:19 2006 +0100
+++ b/src/Pure/pure_thy.ML Sun Nov 26 18:07:16 2006 +0100
@@ -569,12 +569,12 @@
("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", "[tid, sort] => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
("_constrain", "['a, type] => 'a", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", "[id, type] => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtyp", "[id, type] => idt", Mixfix ("_\\<Colon>_", [], 0)),
("_idtypdummy", "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_type_constraint_", "'a", NoSyn),
("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
("==", "['a, 'a] => prop", InfixrName ("\\<equiv>", 2)),
- ("!!", "[idts, prop] => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+ ("all_binder", "[idts, prop] => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
("==>", "[prop, prop] => prop", InfixrName ("\\<Longrightarrow>", 1)),
("_DDDOT", "aprop", Delimfix "\\<dots>"),
("_bigimpl", "[asms, prop] => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
--- a/src/Sequents/LK0.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/Sequents/LK0.thy Sun Nov 26 18:07:16 2006 +0100
@@ -20,7 +20,7 @@
consts
- Trueprop :: "two_seqi"
+ Trueprop :: "two_seqi"
True :: o
False :: o
@@ -50,18 +50,16 @@
"op |" :: "[o, o] => o" (infixr "\<or>" 30)
"op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
"op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
- "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)
+ 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)
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)
+ 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)
local
--- a/src/ZF/Cardinal.thy Fri Nov 24 22:05:19 2006 +0100
+++ b/src/ZF/Cardinal.thy Sun Nov 26 18:07:16 2006 +0100
@@ -33,15 +33,16 @@
Card :: "i=>o"
"Card(i) == (i = |i|)"
-syntax (xsymbols)
- "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
- "lepoll" :: "[i,i] => o" (infixl "\<lesssim>" 50)
- "lesspoll" :: "[i,i] => o" (infixl "\<prec>" 50)
- "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
+notation (xsymbols)
+ eqpoll (infixl "\<approx>" 50) and
+ lepoll (infixl "\<lesssim>" 50) and
+ lesspoll (infixl "\<prec>" 50) and
+ Least (binder "\<mu>" 10)
-syntax (HTML output)
- "eqpoll" :: "[i,i] => o" (infixl "\<approx>" 50)
- "LEAST " :: "[pttrn, o] => i" ("(3\<mu>_./ _)" [0, 10] 10)
+notation (HTML output)
+ eqpoll (infixl "\<approx>" 50) and
+ Least (binder "\<mu>" 10)
+
subsection{*The Schroeder-Bernstein Theorem*}
text{*See Davey and Priestly, page 106*}