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.
tuned declaration order
authorhaftmann
Thu, 19 Aug 2010 10:27:02 +0200
changeset 38547 973506fe2dbd
parent 38546 5c69afe3df06
child 38548 dea0d2cca822
tuned declaration order
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Wed Aug 18 17:03:09 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Aug 19 10:27:02 2010 +0200
@@ -55,20 +55,20 @@
   Trueprop      :: "bool => prop"                   ("(_)" 5)
 
 consts
-  Not           :: "bool => bool"                   ("~ _" [40] 40)
   True          :: bool
   False         :: bool
+  Not           :: "bool => bool"                   ("~ _" [40] 40)
+  "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
+  "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
+  "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
+
+  "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
 
   The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
   Ex            :: "('a => bool) => bool"           (binder "EX " 10)
   Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
 
-  "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
-  "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
-  "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
-  "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
-
 local
isabelle