src/ZF/ex/PropLog.thy

-(*  Title: 	ZF/ex/PropLog.thy
+(*  Title:      ZF/ex/PropLog.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow & Lawrence C Paulson
+    Author:     Tobias Nipkow & Lawrence C Paulson
     Copyright   1993  University of Cambridge
 
 Datatype definition of propositional logic formulae and inductive definition
 of the propositional tautologies.
 *)

 consts
   prop     :: i
 
 datatype
   "prop" = Fls
-         | Var ("n: nat")	                ("#_" [100] 100)
-         | "=>" ("p: prop", "q: prop")		(infixr 90)
+         | Var ("n: nat")                       ("#_" [100] 100)
+         | "=>" ("p: prop", "q: prop")          (infixr 90)
 
 (** The proof system **)
 consts
   thms     :: i => i
-  "|-"     :: [i,i] => o    			(infixl 50)
+  "|-"     :: [i,i] => o                        (infixl 50)
 
 translations
   "H |- p" == "p : thms(H)"
 
 inductive

 
 (** The semantics **)
 consts
   prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
   is_true  :: [i,i] => o
-  "|="     :: [i,i] => o    			(infixl 50)
+  "|="     :: [i,i] => o                        (infixl 50)
   hyps     :: [i,i] => i
 
 defs
 
   prop_rec_def