src/ZF/ex/PropLog.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
     1.1 --- a/src/ZF/ex/PropLog.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/ex/PropLog.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/ex/PropLog.thy
     1.5 +(*  Title:      ZF/ex/PropLog.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow & Lawrence C Paulson
     1.8 +    Author:     Tobias Nipkow & Lawrence C Paulson
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Datatype definition of propositional logic formulae and inductive definition
    1.12 @@ -15,13 +15,13 @@
    1.13  
    1.14  datatype
    1.15    "prop" = Fls
    1.16 -         | Var ("n: nat")	                ("#_" [100] 100)
    1.17 -         | "=>" ("p: prop", "q: prop")		(infixr 90)
    1.18 +         | Var ("n: nat")                       ("#_" [100] 100)
    1.19 +         | "=>" ("p: prop", "q: prop")          (infixr 90)
    1.20  
    1.21  (** The proof system **)
    1.22  consts
    1.23    thms     :: i => i
    1.24 -  "|-"     :: [i,i] => o    			(infixl 50)
    1.25 +  "|-"     :: [i,i] => o                        (infixl 50)
    1.26  
    1.27  translations
    1.28    "H |- p" == "p : thms(H)"
    1.29 @@ -41,7 +41,7 @@
    1.30  consts
    1.31    prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
    1.32    is_true  :: [i,i] => o
    1.33 -  "|="     :: [i,i] => o    			(infixl 50)
    1.34 +  "|="     :: [i,i] => o                        (infixl 50)
    1.35    hyps     :: [i,i] => i
    1.36  
    1.37  defs