src/HOL/HOL.thy
changeset 3947 eb707467f8c5
parent 3842 b55686a7b22c
child 4083 bcff38832d89
     1.1 --- a/src/HOL/HOL.thy	Mon Oct 20 11:22:29 1997 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Oct 20 11:25:39 1997 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4  
     1.5  (** Core syntax **)
     1.6  
     1.7 +global
     1.8 +
     1.9  classes
    1.10    term < logic
    1.11  
    1.12 @@ -33,6 +35,7 @@
    1.13    Not           :: bool => bool                     ("~ _" [40] 40)
    1.14    True, False   :: bool
    1.15    If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    1.16 +  arbitrary     :: 'a
    1.17  
    1.18    (* Binders *)
    1.19  
    1.20 @@ -141,6 +144,8 @@
    1.21  
    1.22  (** Rules and definitions **)
    1.23  
    1.24 +local
    1.25 +
    1.26  rules
    1.27  
    1.28    eq_reflection "(x=y) ==> (x==y)"
    1.29 @@ -179,9 +184,6 @@
    1.30    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
    1.31    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
    1.32  
    1.33 -consts
    1.34 -  arbitrary :: 'a
    1.35 -
    1.36  
    1.37  end
    1.38