# HG changeset patch
# User oheimb
# Date 850498850 -3600
# Node ID 651fce76c86c4ad4da2a495c466c973484bd9a94
# Parent  2fb9659d30ca3779b2632ee681a90abc9e77a8db
adaptions for symbol font

diff -r 2fb9659d30ca -r 651fce76c86c src/HOL/HOL.thy
--- 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 *)
diff -r 2fb9659d30ca -r 651fce76c86c src/HOL/Nat.thy
--- 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
diff -r 2fb9659d30ca -r 651fce76c86c src/HOL/Prod.thy
--- 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
 
diff -r 2fb9659d30ca -r 651fce76c86c src/HOL/Set.thy
--- 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