adaptions for symbol font
authoroheimb
Fri Dec 13 18:40:50 1996 +0100 (1996-12-13)
changeset 2393651fce76c86c
parent 2392 2fb9659d30ca
child 2394 91d8abf108be
adaptions for symbol font
src/HOL/HOL.thy
src/HOL/Nat.thy
src/HOL/Prod.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Fri Dec 13 18:32:07 1996 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Dec 13 18:40:50 1996 +0100
     1.3 @@ -174,9 +174,6 @@
     1.4    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
     1.5    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.6  
     1.7 -(* start 8bit 1 *)
     1.8 -(* end 8bit 1 *)
     1.9 -
    1.10  end
    1.11  
    1.12  
    1.13 @@ -198,6 +195,3 @@
    1.14  
    1.15  val print_ast_translation =
    1.16    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    1.17 -
    1.18 -(* start 8bit 2 *)
    1.19 -(* end 8bit 2 *)
     2.1 --- a/src/HOL/Nat.thy	Fri Dec 13 18:32:07 1996 +0100
     2.2 +++ b/src/HOL/Nat.thy	Fri Dec 13 18:40:50 1996 +0100
     2.3 @@ -56,9 +56,15 @@
     2.4    "2"       :: nat                ("2")
     2.5  
     2.6  translations
     2.7 -   "1"  == "Suc(0)"
     2.8 -   "2"  == "Suc(1)"
     2.9 -  "case p of 0 => a | Suc(y) => b" == "nat_case a (%y.b) p"
    2.10 +   "1"  == "Suc 0"
    2.11 +   "2"  == "Suc 1"
    2.12 +  "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
    2.13 +
    2.14 +(*
    2.15 +syntax (symbols)
    2.16 +
    2.17 +  "LEAST "	:: [idts, bool] => nat		("(3\\<mu>_./ _)" [0, 10] 10)
    2.18 +*)
    2.19  
    2.20  defs
    2.21    Zero_def      "0 == Abs_Nat(Zero_Rep)"
    2.22 @@ -66,8 +72,8 @@
    2.23  
    2.24    (*nat operations and recursion*)
    2.25    nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    2.26 -                                        & (!x. n=Suc(x) --> z=f(x))"
    2.27 -  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    2.28 +                                        & (!x. n=Suc x --> z=f(x))"
    2.29 +  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc n)}"
    2.30  
    2.31    less_def      "m<n == (m,n):trancl(pred_nat)"
    2.32  
    2.33 @@ -76,9 +82,6 @@
    2.34    nat_rec_def   "nat_rec c d ==
    2.35                   wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
    2.36    (*least number operator*)
    2.37 -  Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
    2.38 -
    2.39 -(* start 8bit 1 *)
    2.40 -(* end 8bit 1 *)
    2.41 +  Least_def     "Least P == @k. P(k) & (ALL j. j<k --> ~P(j))"
    2.42  
    2.43  end
     3.1 --- a/src/HOL/Prod.thy	Fri Dec 13 18:32:07 1996 +0100
     3.2 +++ b/src/HOL/Prod.thy	Fri Dec 13 18:40:50 1996 +0100
     3.3 @@ -47,7 +47,6 @@
     3.4    "@pttrn"      :: [pttrn, pttrns] => pttrn     ("'(_,/_')")
     3.5    ""            :: pttrn => pttrns              ("_")
     3.6    "@pttrns"     :: [pttrn, pttrns] => pttrns    ("_,/_")
     3.7 -
     3.8    "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3SIGMA _:_./ _)" 10)
     3.9    "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
    3.10  
    3.11 @@ -70,8 +69,8 @@
    3.12  
    3.13  defs
    3.14    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    3.15 -  fst_def       "fst(p) == @a. ? b. p = (a, b)"
    3.16 -  snd_def       "snd(p) == @b. ? a. p = (a, b)"
    3.17 +  fst_def       "fst p == @a. ? b. p = (a, b)"
    3.18 +  snd_def       "snd p == @b. ? a. p = (a, b)"
    3.19    split_def     "split == (%c p. c (fst p) (snd p))"
    3.20    prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    3.21    Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    3.22 @@ -87,10 +86,7 @@
    3.23    "()"          :: unit                           ("'(')")
    3.24  
    3.25  defs
    3.26 -  Unity_def     "() == Abs_Unit(True)"
    3.27 -
    3.28 -(* start 8bit 1 *)
    3.29 -(* end 8bit 1 *)
    3.30 +  Unity_def     "() == Abs_Unit True"
    3.31  
    3.32  end
    3.33  
     4.1 --- a/src/HOL/Set.thy	Fri Dec 13 18:32:07 1996 +0100
     4.2 +++ b/src/HOL/Set.thy	Fri Dec 13 18:40:50 1996 +0100
     4.3 @@ -127,24 +127,23 @@
     4.4    Ball_def      "Ball A P       == ! x. x:A --> P(x)"
     4.5    Bex_def       "Bex A P        == ? x. x:A & P(x)"
     4.6    subset_def    "A <= B         == ! x:A. x:B"
     4.7 -  Compl_def     "Compl(A)       == {x. ~x:A}"
     4.8 +  Compl_def     "Compl A        == {x. ~x:A}"
     4.9    Un_def        "A Un B         == {x.x:A | x:B}"
    4.10    Int_def       "A Int B        == {x.x:A & x:B}"
    4.11    set_diff_def  "A - B          == {x. x:A & ~x:B}"
    4.12    INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
    4.13    UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
    4.14 -  INTER1_def    "INTER1(B)      == INTER {x.True} B"
    4.15 -  UNION1_def    "UNION1(B)      == UNION {x.True} B"
    4.16 -  Inter_def     "Inter(S)       == (INT x:S. x)"
    4.17 -  Union_def     "Union(S)       == (UN x:S. x)"
    4.18 -  Pow_def       "Pow(A)         == {B. B <= A}"
    4.19 +  INTER1_def    "INTER1 B       == INTER {x.True} B"
    4.20 +  UNION1_def    "UNION1 B       == UNION {x.True} B"
    4.21 +  Inter_def     "Inter S        == (INT x:S. x)"
    4.22 +  Union_def     "Union S        == (UN x:S. x)"
    4.23 +  Pow_def       "Pow A          == {B. B <= A}"
    4.24    empty_def     "{}             == {x. False}"
    4.25    insert_def    "insert a B     == {x.x=a} Un B"
    4.26    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    4.27 -  inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
    4.28 +  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    4.29    inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    4.30 -  surj_def      "surj(f)        == ! y. ? x. y=f(x)"
    4.31 -
    4.32 +  surj_def      "surj f         == ! y. ? x. y=f(x)"
    4.33  
    4.34  end
    4.35