src/HOL/HOL.thy
changeset 2260 b59781f2b809
parent 1674 33aff4d854e4
child 2368 d394336997cf
     1.1 --- a/src/HOL/HOL.thy	Wed Nov 27 16:48:19 1996 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Nov 27 16:51:15 1996 +0100
     1.3 @@ -3,23 +3,17 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -Higher-Order Logic
     1.8 +Higher-Order Logic.
     1.9  *)
    1.10  
    1.11  HOL = CPure +
    1.12  
    1.13 +
    1.14 +(** Core syntax **)
    1.15 +
    1.16  classes
    1.17    term < logic
    1.18  
    1.19 -axclass
    1.20 -  plus < term
    1.21 -
    1.22 -axclass
    1.23 -  minus < term
    1.24 -
    1.25 -axclass
    1.26 -  times < term
    1.27 -
    1.28  default
    1.29    term
    1.30  
    1.31 @@ -57,13 +51,27 @@
    1.32    "|"           :: [bool, bool] => bool             (infixr 30)
    1.33    "-->"         :: [bool, bool] => bool             (infixr 25)
    1.34  
    1.35 -  (* Overloaded Constants *)
    1.36 +
    1.37 +(* Overloaded Constants *)
    1.38 +
    1.39 +axclass
    1.40 +  plus < term
    1.41  
    1.42 +axclass
    1.43 +  minus < term
    1.44 +
    1.45 +axclass
    1.46 +  times < term
    1.47 +
    1.48 +consts
    1.49    "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
    1.50    "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    1.51    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.52  
    1.53  
    1.54 +
    1.55 +(** Additional concrete syntax **)
    1.56 +
    1.57  types
    1.58    letbinds  letbind
    1.59    case_syn  cases_syn
    1.60 @@ -72,7 +80,7 @@
    1.61  
    1.62    "~="          :: ['a, 'a] => bool                 (infixl 50)
    1.63  
    1.64 -  "@Eps"        :: [pttrn,bool] => 'a               ("(3@ _./ _)" 10)
    1.65 +  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" 10)
    1.66  
    1.67    (* Alternative Quantifiers *)
    1.68  
    1.69 @@ -96,13 +104,34 @@
    1.70  
    1.71  translations
    1.72    "x ~= y"      == "~ (x = y)"
    1.73 -  "@ x.b"       == "Eps(%x.b)"
    1.74 +  "@ x.b"       == "Eps (%x. b)"
    1.75    "ALL xs. P"   => "! xs. P"
    1.76    "EX xs. P"    => "? xs. P"
    1.77    "EX! xs. P"   => "?! xs. P"
    1.78    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    1.79    "let x = a in e"        == "Let a (%x. e)"
    1.80  
    1.81 +
    1.82 +syntax (symbols)
    1.83 +  not           :: bool => bool                     ("\\<not> _" [40] 40)
    1.84 +  "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
    1.85 +  "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
    1.86 +  "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.87 +  "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
    1.88 +  "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
    1.89 +  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" 10)
    1.90 +  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
    1.91 +  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
    1.92 +  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
    1.93 +  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
    1.94 +  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
    1.95 +  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
    1.96 +  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
    1.97 +
    1.98 +
    1.99 +
   1.100 +(** Rules and definitions **)
   1.101 +
   1.102  rules
   1.103  
   1.104    eq_reflection "(x=y) ==> (x==y)"
   1.105 @@ -147,6 +176,7 @@
   1.106  
   1.107  end
   1.108  
   1.109 +
   1.110  ML
   1.111  
   1.112  (** Choice between the HOL and Isabelle style of quantifiers **)
   1.113 @@ -168,6 +198,3 @@
   1.114  
   1.115  (* start 8bit 2 *)
   1.116  (* end 8bit 2 *)
   1.117 -
   1.118 -
   1.119 -