1.1 --- a/src/FOL/IFOL.thy	Wed Oct 06 14:45:04 1993 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Thu Oct 07 09:47:47 1993 +0100
     1.3 @@ -1,3 +1,11 @@
     1.4 +(*  Title: 	FOL/ifol.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Intuitionistic first-order logic
    1.10 +*)
    1.11 +
    1.12  IFOL = Pure + 
    1.13  
    1.14  classes term < logic
    1.15 @@ -10,19 +18,24 @@
    1.16  
    1.17  consts	
    1.18      Trueprop	::	"o => prop"		("(_)" [0] 5)
    1.19 -    True,False	::	"o"
    1.20 +    True, False	::	"o"
    1.21    (*Connectives*)
    1.22 -    "="		::	"['a,'a] => o"		(infixl 50)
    1.23 +    "=", "~="	::	"['a,'a] => o"		(infixl 50)
    1.24 +
    1.25      Not		::	"o => o"		("~ _" [40] 40)
    1.26      "&"		::	"[o,o] => o"		(infixr 35)
    1.27      "|"		::	"[o,o] => o"		(infixr 30)
    1.28      "-->"	::	"[o,o] => o"		(infixr 25)
    1.29      "<->"	::	"[o,o] => o"		(infixr 25)
    1.30 +  
    1.31    (*Quantifiers*)
    1.32      All		::	"('a => o) => o"	(binder "ALL " 10)
    1.33      Ex		::	"('a => o) => o"	(binder "EX " 10)
    1.34      Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    1.35  
    1.36 +translations
    1.37 +    "x ~= y"    == "~ (x=y)"
    1.38 +
    1.39  rules
    1.40  
    1.41    (*Equality*)
    1.42 @@ -47,8 +60,8 @@
    1.43  
    1.44    (*Definitions*)
    1.45  
    1.46 -True_def	"True == False-->False"
    1.47 -not_def		"~P == P-->False"
    1.48 +True_def	"True  == False-->False"
    1.49 +not_def		"~P    == P-->False"
    1.50  iff_def		"P<->Q == (P-->Q) & (Q-->P)"
    1.51  
    1.52    (*Unique existence*)

     2.1 --- a/src/FOL/ifol.thy	Wed Oct 06 14:45:04 1993 +0100
     2.2 +++ b/src/FOL/ifol.thy	Thu Oct 07 09:47:47 1993 +0100
     2.3 @@ -1,3 +1,11 @@
     2.4 +(*  Title: 	FOL/ifol.thy
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1993  University of Cambridge
     2.8 +
     2.9 +Intuitionistic first-order logic
    2.10 +*)
    2.11 +
    2.12  IFOL = Pure + 
    2.13  
    2.14  classes term < logic
    2.15 @@ -10,19 +18,24 @@
    2.16  
    2.17  consts	
    2.18      Trueprop	::	"o => prop"		("(_)" [0] 5)
    2.19 -    True,False	::	"o"
    2.20 +    True, False	::	"o"
    2.21    (*Connectives*)
    2.22 -    "="		::	"['a,'a] => o"		(infixl 50)
    2.23 +    "=", "~="	::	"['a,'a] => o"		(infixl 50)
    2.24 +
    2.25      Not		::	"o => o"		("~ _" [40] 40)
    2.26      "&"		::	"[o,o] => o"		(infixr 35)
    2.27      "|"		::	"[o,o] => o"		(infixr 30)
    2.28      "-->"	::	"[o,o] => o"		(infixr 25)
    2.29      "<->"	::	"[o,o] => o"		(infixr 25)
    2.30 +  
    2.31    (*Quantifiers*)
    2.32      All		::	"('a => o) => o"	(binder "ALL " 10)
    2.33      Ex		::	"('a => o) => o"	(binder "EX " 10)
    2.34      Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    2.35  
    2.36 +translations
    2.37 +    "x ~= y"    == "~ (x=y)"
    2.38 +
    2.39  rules
    2.40  
    2.41    (*Equality*)
    2.42 @@ -47,8 +60,8 @@
    2.43  
    2.44    (*Definitions*)
    2.45  
    2.46 -True_def	"True == False-->False"
    2.47 -not_def		"~P == P-->False"
    2.48 +True_def	"True  == False-->False"
    2.49 +not_def		"~P    == P-->False"
    2.50  iff_def		"P<->Q == (P-->Q) & (Q-->P)"
    2.51  
    2.52    (*Unique existence*)