diff -r 000000000000 -r 7949f97df77a hol.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hol.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,142 @@
+(*  Title:      HOL/hol.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1993  University of Cambridge
+
+Higher-Order Logic
+*)
+
+HOL = Pure +
+
+classes
+  term < logic
+  plus < term
+  minus < term
+  times < term
+
+default term
+
+types
+  bool 0
+
+arities
+  fun :: (term, term) term
+  bool :: term
+
+
+consts
+
+  (* Constants *)
+
+  Trueprop      :: "bool => prop"                       ("(_)" [0] 5)
+  not           :: "bool => bool"                       ("~ _" [40] 40)
+  True, False   :: "bool"
+  if            :: "[bool, 'a, 'a] => 'a"
+  Inv           :: "('a => 'b) => ('b => 'a)"
+
+  (* Binders *)
+
+  Eps           :: "('a => bool) => 'a"                 (binder "@" 10)
+  All           :: "('a => bool) => bool"               (binder "! " 10)
+  Ex            :: "('a => bool) => bool"               (binder "? " 10)
+  Ex1           :: "('a => bool) => bool"               (binder "?! " 10)
+
+  Let		:: "['a, 'a=>'b] => 'b"
+  "@let"	:: "[idt,'a,'b] => 'b"		("(let _ = (2_)/ in (2_))" 10)
+
+  (* Alternative Quantifiers *)
+
+  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" [0,0] 10)
+  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" [0,0] 10)
+  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" [0,0] 10)
+
+  (* Infixes *)
+
+  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50)
+  "="           :: "['a, 'a] => bool"                   (infixl 50)
+  "&"           :: "[bool, bool] => bool"               (infixr 35)
+  "|"           :: "[bool, bool] => bool"               (infixr 30)
+  "-->"         :: "[bool, bool] => bool"               (infixr 25)
+
+  (* Overloaded Constants *)
+
+  "+"           :: "['a::plus, 'a] => 'a"               (infixl 65)
+  "-"           :: "['a::minus, 'a] => 'a"              (infixl 65)
+  "*"           :: "['a::times, 'a] => 'a"              (infixl 70)
+
+  (* Rewriting Gadget *)
+
+  NORM          :: "'a => 'a"
+
+
+translations
+  "ALL xs. P"   => "! xs. P"
+  "EX xs. P"    => "? xs. P"
+  "EX! xs. P"   => "?! xs. P"
+
+  "let x = s in t" == "Let(s,%x.t)"
+
+rules
+
+  eq_reflection "(x=y) ==> (x==y)"
+
+  (* Basic Rules *)
+
+  refl          "t = t::'a"
+  subst         "[| s = t; P(s) |] ==> P(t::'a)"
+  ext           "(!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))"
+  selectI       "P(x::'a) ==> P(@x.P(x))"
+
+  impI          "(P ==> Q) ==> P-->Q"
+  mp            "[| P-->Q;  P |] ==> Q"
+
+  (* Definitions *)
+
+  True_def      "True = ((%x.x)=(%x.x))"
+  All_def       "All  = (%P. P = (%x.True))"
+  Ex_def        "Ex   = (%P. P(@x.P(x)))"
+  False_def     "False = (!P.P)"
+  not_def       "not  = (%P. P-->False)"
+  and_def       "op & = (%P Q. !R. (P-->Q-->R) --> R)"
+  or_def        "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
+  Ex1_def       "Ex1  = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
+  Let_def	"Let(s,f) = f(s)"
+
+  (* Axioms *)
+
+  iff           "(P-->Q) --> (Q-->P) --> (P=Q)"
+  True_or_False "(P=True) | (P=False)"
+
+  (* Misc Definitions *)
+
+  Inv_def       "Inv = (%(f::'a=>'b) y. @x. f(x)=y)"
+  o_def         "op o = (%(f::'b=>'c) g (x::'a). f(g(x)))"
+
+  if_def        "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+
+  (* Rewriting -- special constant to flag normalized terms *)
+
+  NORM_def      "NORM(x) = x"
+
+end
+
+
+ML
+
+(** Choice between the HOL and Isabelle style of quantifiers **)
+
+val HOL_quantifiers = ref true;
+
+fun mk_alt_ast_tr' (name, alt_name) =
+  let
+    fun ast_tr' (*name*) args =
+      if ! HOL_quantifiers then raise Match
+      else Ast.mk_appl (Ast.Constant alt_name) args;
+  in
+    (name, ast_tr')
+  end;
+
+
+val print_ast_translation =
+  map mk_alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
+