# HG changeset patch
# User lcp
# Date 749983667 -3600
# Node ID d71f96f1780eb81f69d36966f31a6b1898e17dd6
# Parent  747f1aad03cf0a284732fe395f0ab89cf202d181
ifol.thy: added ~= for "not equals"

diff -r 747f1aad03cf -r d71f96f1780e src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Oct 06 14:45:04 1993 +0100
+++ b/src/FOL/IFOL.thy	Thu Oct 07 09:47:47 1993 +0100
@@ -1,3 +1,11 @@
+(*  Title: 	FOL/ifol.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Intuitionistic first-order logic
+*)
+
 IFOL = Pure + 
 
 classes term < logic
@@ -10,19 +18,24 @@
 
 consts	
     Trueprop	::	"o => prop"		("(_)" [0] 5)
-    True,False	::	"o"
+    True, False	::	"o"
   (*Connectives*)
-    "="		::	"['a,'a] => o"		(infixl 50)
+    "=", "~="	::	"['a,'a] => o"		(infixl 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)
 
+translations
+    "x ~= y"    == "~ (x=y)"
+
 rules
 
   (*Equality*)
@@ -47,8 +60,8 @@
 
   (*Definitions*)
 
-True_def	"True == False-->False"
-not_def		"~P == P-->False"
+True_def	"True  == False-->False"
+not_def		"~P    == P-->False"
 iff_def		"P<->Q == (P-->Q) & (Q-->P)"
 
   (*Unique existence*)
diff -r 747f1aad03cf -r d71f96f1780e src/FOL/ifol.thy
--- a/src/FOL/ifol.thy	Wed Oct 06 14:45:04 1993 +0100
+++ b/src/FOL/ifol.thy	Thu Oct 07 09:47:47 1993 +0100
@@ -1,3 +1,11 @@
+(*  Title: 	FOL/ifol.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Intuitionistic first-order logic
+*)
+
 IFOL = Pure + 
 
 classes term < logic
@@ -10,19 +18,24 @@
 
 consts	
     Trueprop	::	"o => prop"		("(_)" [0] 5)
-    True,False	::	"o"
+    True, False	::	"o"
   (*Connectives*)
-    "="		::	"['a,'a] => o"		(infixl 50)
+    "=", "~="	::	"['a,'a] => o"		(infixl 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)
 
+translations
+    "x ~= y"    == "~ (x=y)"
+
 rules
 
   (*Equality*)
@@ -47,8 +60,8 @@
 
   (*Definitions*)
 
-True_def	"True == False-->False"
-not_def		"~P == P-->False"
+True_def	"True  == False-->False"
+not_def		"~P    == P-->False"
 iff_def		"P<->Q == (P-->Q) & (Q-->P)"
 
   (*Unique existence*)