--- a/src/FOL/IFOL.thy Sat Apr 08 22:12:02 2006 +0200
+++ b/src/FOL/IFOL.thy Sat Apr 08 22:51:06 2006 +0200
@@ -45,10 +45,18 @@
Ex1 :: "('a => o) => o" (binder "EX! " 10)
-abbreviation (output)
+abbreviation
not_equal :: "['a, 'a] => o" (infixl "~=" 50)
"x ~= y == ~ (x = y)"
+abbreviation (xsymbols)
+ not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+ "x \<noteq> y == ~ (x = y)"
+
+abbreviation (HTML output)
+ not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+ "not_equal == xsymbols.not_equal"
+
syntax (xsymbols)
Not :: "o => o" ("\<not> _" [40] 40)
"op &" :: "[o, o] => o" (infixr "\<and>" 35)
@@ -56,7 +64,6 @@
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
"op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
"op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
@@ -67,7 +74,6 @@
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
local