Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Name of ML function "not" is now qualified in order to avoid
authorberghofe
Thu, 10 May 2007 15:49:31 +0200
changeset 22922 66baa75eae06
parent 22921 475ff421a6a3
child 22923 6384c43da028
Name of ML function "not" is now qualified in order to avoid clashes with names of constants introduced by the user.
src/HOL/Code_Generator.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Code_Generator.thy	Thu May 10 10:22:17 2007 +0200
+++ b/src/HOL/Code_Generator.thy	Thu May 10 15:49:31 2007 +0200
@@ -36,7 +36,7 @@
   "Trueprop" ("(_)")
   "True"    ("true")
   "False"   ("false")
-  "Not"     ("not")
+  "Not"     ("Bool.not")
   "op |"    ("(_ orelse/ _)")
   "op &"    ("(_ andalso/ _)")
   "If"      ("(if _/ then _/ else _)")
isabelle