1.1 --- a/src/HOL/IMP/BExp.thy	Sun Oct 23 14:03:37 2011 +0200
     1.2 +++ b/src/HOL/IMP/BExp.thy	Sun Oct 23 14:15:24 2011 +0200
     1.3 @@ -72,10 +72,10 @@
     1.4  
     1.5  text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbsimpdef}{% *}
     1.6  fun bsimp :: "bexp \<Rightarrow> bexp" where
     1.7 -"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)" |
     1.8 +"bsimp (Bc v) = Bc v" |
     1.9 +"bsimp (Not b) = not(bsimp b)" |
    1.10  "bsimp (And b\<^isub>1 b\<^isub>2) = and (bsimp b\<^isub>1) (bsimp b\<^isub>2)" |
    1.11 -"bsimp (Not b) = not(bsimp b)" |
    1.12 -"bsimp (Bc v) = Bc v"
    1.13 +"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)"
    1.14  text_raw{*}\end{isaverbatimwrite}*}
    1.15  
    1.16  value "bsimp (And (Less (N 0) (N 1)) b)"