--- a/src/HOL/HOL.thy Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/HOL.thy Thu Aug 26 20:51:17 2010 +0200
@@ -56,13 +56,13 @@
True :: bool
False :: bool
Not :: "bool => bool" ("~ _" [40] 40)
+ implies :: "[bool, bool] => bool" (infixr "-->" 25)
setup Sign.root_path
consts
"op &" :: "[bool, bool] => bool" (infixr "&" 35)
"op |" :: "[bool, bool] => bool" (infixr "|" 30)
- "op -->" :: "[bool, bool] => bool" (infixr "-->" 25)
"op =" :: "['a, 'a] => bool" (infixl "=" 50)
@@ -91,7 +91,7 @@
Not ("\<not> _" [40] 40) and
"op &" (infixr "\<and>" 35) and
"op |" (infixr "\<or>" 30) and
- "op -->" (infixr "\<longrightarrow>" 25) and
+ HOL.implies (infixr "\<longrightarrow>" 25) and
not_equal (infix "\<noteq>" 50)
notation (HTML output)
@@ -184,7 +184,7 @@
finalconsts
"op ="
- "op -->"
+ HOL.implies
The
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where