# HG changeset patch
# User haftmann
# Date 1282206422 -7200
# Node ID 973506fe2dbd358348b37cda95e656fb6b7fa304
# Parent  5c69afe3df06f4d682594c2d6da503985316db0f
tuned declaration order

diff -r 5c69afe3df06 -r 973506fe2dbd src/HOL/HOL.thy
--- 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