# HG changeset patch
# User nipkow
# Date 1319372124 -7200
# Node ID 62b025f434e903ea71ea1c092ea8f6ed05d0c592
# Parent  ffc06165d2720f9da52cdd2c1cb075316a3a0d63
tuned order of eqns

diff -r ffc06165d272 -r 62b025f434e9 src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Sun Oct 23 14:03:37 2011 +0200
+++ b/src/HOL/IMP/BExp.thy	Sun Oct 23 14:15:24 2011 +0200
@@ -72,10 +72,10 @@
 
 text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbsimpdef}{% *}
 fun bsimp :: "bexp \<Rightarrow> bexp" where
-"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)" |
+"bsimp (Bc v) = Bc v" |
+"bsimp (Not b) = not(bsimp b)" |
 "bsimp (And b\<^isub>1 b\<^isub>2) = and (bsimp b\<^isub>1) (bsimp b\<^isub>2)" |
-"bsimp (Not b) = not(bsimp b)" |
-"bsimp (Bc v) = Bc v"
+"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)"
 text_raw{*}\end{isaverbatimwrite}*}
 
 value "bsimp (And (Less (N 0) (N 1)) b)"