--- a/src/HOL/HOL.thy Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/HOL.thy Fri Aug 27 10:56:46 2010 +0200
@@ -56,14 +56,14 @@
True :: bool
False :: bool
Not :: "bool => bool" ("~ _" [40] 40)
+
+ conj :: "[bool, bool] => bool" (infixr "&" 35)
+ disj :: "[bool, bool] => bool" (infixr "|" 30)
implies :: "[bool, bool] => bool" (infixr "-->" 25)
setup Sign.root_path
consts
- "op &" :: "[bool, bool] => bool" (infixr "&" 35)
- "op |" :: "[bool, bool] => bool" (infixr "|" 30)
-
"op =" :: "['a, 'a] => bool" (infixl "=" 50)
setup Sign.local_path
@@ -89,15 +89,15 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ HOL.conj (infixr "\<and>" 35) and
+ HOL.disj (infixr "\<or>" 30) and
HOL.implies (infixr "\<longrightarrow>" 25) and
not_equal (infix "\<noteq>" 50)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ HOL.conj (infixr "\<and>" 35) and
+ HOL.disj (infixr "\<or>" 30) and
not_equal (infix "\<noteq>" 50)
abbreviation (iff)
@@ -1578,7 +1578,7 @@
val atomize_conjL = @{thm atomize_conjL}
val atomize_disjL = @{thm atomize_disjL}
val operator_names =
- [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
+ [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
);
*}
@@ -1737,8 +1737,8 @@
"True" ("true")
"False" ("false")
"Not" ("Bool.not")
- "op |" ("(_ orelse/ _)")
- "op &" ("(_ andalso/ _)")
+ HOL.disj ("(_ orelse/ _)")
+ HOL.conj ("(_ andalso/ _)")
"If" ("(if _/ then _/ else _)")
setup {*
@@ -1914,7 +1914,7 @@
(Haskell "Bool")
(Scala "Boolean")
-code_const True and False and Not and "op &" and "op |" and If
+code_const True and False and Not and HOL.conj and HOL.disj and If
(SML "true" and "false" and "not"
and infixl 1 "andalso" and infixl 0 "orelse"
and "!(if (_)/ then (_)/ else (_))")