src/FOL/IFOL.thy
changeset 35 d71f96f1780e
parent 0 a5a9c433f639
child 79 74e68ed3b4fd
     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*)