--- a/src/HOL/HOL.thy Fri Dec 13 18:32:07 1996 +0100
+++ b/src/HOL/HOL.thy Fri Dec 13 18:40:50 1996 +0100
@@ -174,9 +174,6 @@
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)"
-(* start 8bit 1 *)
-(* end 8bit 1 *)
-
end
@@ -198,6 +195,3 @@
val print_ast_translation =
map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
-
-(* start 8bit 2 *)
-(* end 8bit 2 *)
--- a/src/HOL/Nat.thy Fri Dec 13 18:32:07 1996 +0100
+++ b/src/HOL/Nat.thy Fri Dec 13 18:40:50 1996 +0100
@@ -56,9 +56,15 @@
"2" :: nat ("2")
translations
- "1" == "Suc(0)"
- "2" == "Suc(1)"
- "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
+ "1" == "Suc 0"
+ "2" == "Suc 1"
+ "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
+
+(*
+syntax (symbols)
+
+ "LEAST " :: [idts, bool] => nat ("(3\\<mu>_./ _)" [0, 10] 10)
+*)
defs
Zero_def "0 == Abs_Nat(Zero_Rep)"
@@ -66,8 +72,8 @@
(*nat operations and recursion*)
nat_case_def "nat_case a f n == @z. (n=0 --> z=a)
- & (!x. n=Suc(x) --> z=f(x))"
- pred_nat_def "pred_nat == {p. ? n. p = (n, Suc(n))}"
+ & (!x. n=Suc x --> z=f(x))"
+ pred_nat_def "pred_nat == {p. ? n. p = (n, Suc n)}"
less_def "m<n == (m,n):trancl(pred_nat)"
@@ -76,9 +82,6 @@
nat_rec_def "nat_rec c d ==
wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
(*least number operator*)
- Least_def "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
-
-(* start 8bit 1 *)
-(* end 8bit 1 *)
+ Least_def "Least P == @k. P(k) & (ALL j. j<k --> ~P(j))"
end
--- a/src/HOL/Prod.thy Fri Dec 13 18:32:07 1996 +0100
+++ b/src/HOL/Prod.thy Fri Dec 13 18:40:50 1996 +0100
@@ -47,7 +47,6 @@
"@pttrn" :: [pttrn, pttrns] => pttrn ("'(_,/_')")
"" :: pttrn => pttrns ("_")
"@pttrns" :: [pttrn, pttrns] => pttrns ("_,/_")
-
"@Sigma" :: "[idt, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80)
@@ -70,8 +69,8 @@
defs
Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)"
- fst_def "fst(p) == @a. ? b. p = (a, b)"
- snd_def "snd(p) == @b. ? a. p = (a, b)"
+ fst_def "fst p == @a. ? b. p = (a, b)"
+ snd_def "snd p == @b. ? a. p = (a, b)"
split_def "split == (%c p. c (fst p) (snd p))"
prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))"
Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
@@ -87,10 +86,7 @@
"()" :: unit ("'(')")
defs
- Unity_def "() == Abs_Unit(True)"
-
-(* start 8bit 1 *)
-(* end 8bit 1 *)
+ Unity_def "() == Abs_Unit True"
end
--- a/src/HOL/Set.thy Fri Dec 13 18:32:07 1996 +0100
+++ b/src/HOL/Set.thy Fri Dec 13 18:40:50 1996 +0100
@@ -127,24 +127,23 @@
Ball_def "Ball A P == ! x. x:A --> P(x)"
Bex_def "Bex A P == ? x. x:A & P(x)"
subset_def "A <= B == ! x:A. x:B"
- Compl_def "Compl(A) == {x. ~x:A}"
+ Compl_def "Compl A == {x. ~x:A}"
Un_def "A Un B == {x.x:A | x:B}"
Int_def "A Int B == {x.x:A & x:B}"
set_diff_def "A - B == {x. x:A & ~x:B}"
INTER_def "INTER A B == {y. ! x:A. y: B(x)}"
UNION_def "UNION A B == {y. ? x:A. y: B(x)}"
- INTER1_def "INTER1(B) == INTER {x.True} B"
- UNION1_def "UNION1(B) == UNION {x.True} B"
- Inter_def "Inter(S) == (INT x:S. x)"
- Union_def "Union(S) == (UN x:S. x)"
- Pow_def "Pow(A) == {B. B <= A}"
+ INTER1_def "INTER1 B == INTER {x.True} B"
+ UNION1_def "UNION1 B == UNION {x.True} B"
+ Inter_def "Inter S == (INT x:S. x)"
+ Union_def "Union S == (UN x:S. x)"
+ Pow_def "Pow A == {B. B <= A}"
empty_def "{} == {x. False}"
insert_def "insert a B == {x.x=a} Un B"
image_def "f``A == {y. ? x:A. y=f(x)}"
- inj_def "inj(f) == ! x y. f(x)=f(y) --> x=y"
+ inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
- surj_def "surj(f) == ! y. ? x. y=f(x)"
-
+ surj_def "surj f == ! y. ? x. y=f(x)"
end