diff -r e76a1edc2e49 -r 74e68ed3b4fd src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Oct 22 22:17:25 1993 +0100
+++ b/src/FOL/IFOL.thy	Mon Oct 25 12:32:53 1993 +0100
@@ -1,83 +1,97 @@
-(*  Title: 	FOL/ifol.thy
+(*  Title:      FOL/ifol.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Intuitionistic first-order logic
 *)
 
-IFOL = Pure + 
+IFOL = Pure +
 
-classes term < logic
+classes
+  term < logic
+
+default
+  term
 
-default term
+types
+  o 0
 
-types o 0
+arities
+  o :: logic
 
-arities o :: logic
+
+consts
 
-consts	
-    Trueprop	::	"o => prop"		("(_)" [0] 5)
-    True, False	::	"o"
-  (*Connectives*)
-    "=", "~="	::	"['a,'a] => o"		(infixl 50)
+  Trueprop      :: "o => prop"                  ("(_)" 5)
+  True, False   :: "o"
+
+  (* Connectives *)
+
+  "="           :: "['a, 'a] => o"              (infixl 50)
+  "~="          :: "['a, 'a] => o"              ("(_ ~=/ _)" [50, 51] 50)
 
-    Not		::	"o => o"		("~ _" [40] 40)
-    "&"		::	"[o,o] => o"		(infixr 35)
-    "|"		::	"[o,o] => o"		(infixr 30)
-    "-->"	::	"[o,o] => o"		(infixr 25)
-    "<->"	::	"[o,o] => o"		(infixr 25)
-  
-  (*Quantifiers*)
-    All		::	"('a => o) => o"	(binder "ALL " 10)
-    Ex		::	"('a => o) => o"	(binder "EX " 10)
-    Ex1		::	"('a => o) => o"	(binder "EX! " 10)
+  Not           :: "o => o"                     ("~ _" [40] 40)
+  "&"           :: "[o, o] => o"                (infixr 35)
+  "|"           :: "[o, o] => o"                (infixr 30)
+  "-->"         :: "[o, o] => o"                (infixr 25)
+  "<->"         :: "[o, o] => o"                (infixr 25)
+
+  (* Quantifiers *)
+
+  All           :: "('a => o) => o"             (binder "ALL " 10)
+  Ex            :: "('a => o) => o"             (binder "EX " 10)
+  Ex1           :: "('a => o) => o"             (binder "EX! " 10)
+
 
 translations
-    "x ~= y"    == "~ (x=y)"
+  "x ~= y"      == "~ (x = y)"
+
 
 rules
 
-  (*Equality*)
+  (* Equality *)
 
-refl		"a=a"
-subst		"[| a=b;  P(a) |] ==> P(b)"
+  refl          "a=a"
+  subst         "[| a=b;  P(a) |] ==> P(b)"
 
-  (*Propositional logic*)
+  (* Propositional logic *)
 
-conjI		"[| P;  Q |] ==> P&Q"
-conjunct1	"P&Q ==> P"
-conjunct2	"P&Q ==> Q"
+  conjI         "[| P;  Q |] ==> P&Q"
+  conjunct1     "P&Q ==> P"
+  conjunct2     "P&Q ==> Q"
 
-disjI1		"P ==> P|Q"
-disjI2		"Q ==> P|Q"
-disjE		"[| P|Q;  P ==> R;  Q ==> R |] ==> R"
+  disjI1        "P ==> P|Q"
+  disjI2        "Q ==> P|Q"
+  disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
 
-impI		"(P ==> Q) ==> P-->Q"
-mp		"[| P-->Q;  P |] ==> Q"
+  impI          "(P ==> Q) ==> P-->Q"
+  mp            "[| P-->Q;  P |] ==> Q"
 
-FalseE		"False ==> P"
+  FalseE        "False ==> P"
 
-  (*Definitions*)
+  (* Definitions *)
 
-True_def	"True  == False-->False"
-not_def		"~P    == P-->False"
-iff_def		"P<->Q == (P-->Q) & (Q-->P)"
+  True_def      "True  == False-->False"
+  not_def       "~P    == P-->False"
+  iff_def       "P<->Q == (P-->Q) & (Q-->P)"
+
+  (* Unique existence *)
 
-  (*Unique existence*)
-ex1_def		"EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+  ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
 
-  (*Quantifiers*)
+  (* Quantifiers *)
 
-allI		"(!!x. P(x)) ==> (ALL x.P(x))"
-spec		"(ALL x.P(x)) ==> P(x)"
+  allI          "(!!x. P(x)) ==> (ALL x.P(x))"
+  spec          "(ALL x.P(x)) ==> P(x)"
 
-exI		"P(x) ==> (EX x.P(x))"
-exE		"[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
+  exI           "P(x) ==> (EX x.P(x))"
+  exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
 
   (* Reflection *)
 
-eq_reflection  "(x=y)   ==> (x==y)"
-iff_reflection "(P<->Q) ==> (P==Q)"
+  eq_reflection   "(x=y)   ==> (x==y)"
+  iff_reflection  "(P<->Q) ==> (P==Q)"
 
 end
+