--- a/src/HOL/HOL.thy Thu Oct 09 15:01:11 1997 +0200
+++ b/src/HOL/HOL.thy Thu Oct 09 15:03:06 1997 +0200
@@ -25,10 +25,6 @@
bool :: term
-syntax ("" output)
- "op =" :: ['a, 'a] => bool ("(_ =/ _)" [51, 51] 50)
- "op ~=" :: ['a, 'a] => bool ("(_ ~=/ _)" [51, 51] 50)
-
consts
(* Constants *)
@@ -75,6 +71,7 @@
"*" :: ['a::times, 'a] => 'a (infixl 70)
(*See Nat.thy for "^"*)
+
(** Additional concrete syntax **)
types
@@ -116,11 +113,9 @@
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
"let x = a in e" == "Let a (%x. e)"
-syntax (symbols output)
- "op ~=" :: ['a, 'a] => bool ("(_ \\<noteq>/ _)" [51, 51] 50)
- "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
- "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
- "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
+syntax ("" output)
+ "op =" :: ['a, 'a] => bool ("(_ =/ _)" [51, 51] 50)
+ "op ~=" :: ['a, 'a] => bool ("(_ ~=/ _)" [51, 51] 50)
syntax (symbols)
Not :: bool => bool ("\\<not> _" [40] 40)
@@ -136,6 +131,12 @@
"@case1" :: ['a, 'b] => case_syn ("(2_ \\<Rightarrow>/ _)" 10)
(*"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\<orelse> _")*)
+syntax (symbols output)
+ "op ~=" :: ['a, 'a] => bool ("(_ \\<noteq>/ _)" [51, 51] 50)
+ "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
+ "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
+ "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
+
(** Rules and definitions **)
@@ -178,8 +179,9 @@
o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
-constdefs arbitrary :: 'a
- "arbitrary == @x.False"
+consts
+ arbitrary :: 'a
+
end
--- a/src/HOL/Ord.thy Thu Oct 09 15:01:11 1997 +0200
+++ b/src/HOL/Ord.thy Thu Oct 09 15:03:06 1997 +0200
@@ -11,6 +11,10 @@
axclass
ord < term
+syntax
+ "op <" :: ['a::ord, 'a] => bool ("op <")
+ "op <=" :: ['a::ord, 'a] => bool ("op <=")
+
consts
"op <" :: ['a::ord, 'a] => bool ("(_/ < _)" [50, 51] 50)
"op <=" :: ['a::ord, 'a] => bool ("(_/ <= _)" [50, 51] 50)
@@ -19,13 +23,10 @@
Least :: ('a::ord=>bool) => 'a (binder "LEAST " 10)
-syntax
- "op <" :: ['a::ord, 'a] => bool ("op <")
- "op <=" :: ['a::ord, 'a] => bool ("op <=")
+syntax (symbols)
+ "op <=" :: ['a::ord, 'a] => bool ("op \\<le>")
+ "op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50)
-syntax (symbols)
- "op <=" :: ['a::ord, 'a] => bool ("(_/ \\<le> _)" [50, 51] 50)
- "op <=" :: ['a::ord, 'a] => bool ("op \\<le>")
defs
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
--- a/src/HOL/Set.thy Thu Oct 09 15:01:11 1997 +0200
+++ b/src/HOL/Set.thy Thu Oct 09 15:03:06 1997 +0200
@@ -18,6 +18,9 @@
instance
set :: (term) {ord, minus, power}
+syntax
+ "op :" :: ['a, 'a set] => bool ("op :")
+
consts
"{}" :: 'a set ("{}")
insert :: ['a, 'a set] => 'a set
@@ -42,14 +45,12 @@
syntax
- "op :" :: ['a, 'a set] => bool ("op :")
-
UNIV :: 'a set
(* Infix syntax for non-membership *)
+ "op ~:" :: ['a, 'a set] => bool ("op ~:")
"op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50)
- "op ~:" :: ['a, 'a set] => bool ("op ~:")
"@Finset" :: args => 'a set ("{(_)}")
@@ -83,22 +84,22 @@
"EX x:A. P" => "Bex A (%x. P)"
syntax ("" output)
+ "_setle" :: ['a set, 'a set] => bool ("op <=")
"_setle" :: ['a set, 'a set] => bool ("(_/ <= _)" [50, 51] 50)
- "_setle" :: ['a set, 'a set] => bool ("op <=")
+ "_setless" :: ['a set, 'a set] => bool ("op <")
"_setless" :: ['a set, 'a set] => bool ("(_/ < _)" [50, 51] 50)
- "_setless" :: ['a set, 'a set] => bool ("op <")
syntax (symbols)
+ "_setle" :: ['a set, 'a set] => bool ("op \\<subseteq>")
"_setle" :: ['a set, 'a set] => bool ("(_/ \\<subseteq> _)" [50, 51] 50)
- "_setle" :: ['a set, 'a set] => bool ("op \\<subseteq>")
+ "_setless" :: ['a set, 'a set] => bool ("op \\<subset>")
"_setless" :: ['a set, 'a set] => bool ("(_/ \\<subset> _)" [50, 51] 50)
- "_setless" :: ['a set, 'a set] => bool ("op \\<subset>")
"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 \\<in>")
+ "op ~:" :: ['a, 'a set] => bool ("op \\<notin>")
"op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50)
- "op ~:" :: ['a, 'a set] => bool ("op \\<notin>")
"UN " :: [idts, bool] => bool ("(3\\<Union> _./ _)" 10)
"INT " :: [idts, bool] => bool ("(3\\<Inter> _./ _)" 10)
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union> _\\<in>_./ _)" 10)