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 definition
authorkleing
Wed, 19 Feb 2014 22:02:00 +1100
changeset 55582 20054fc56d17
parent 55581 d1c228753d76
child 55583 a0134252ac29
tuned definition
src/HOL/IMP/Compiler.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/IMP/Compiler.thy	Wed Feb 19 12:04:21 2014 +0100
+++ b/src/HOL/IMP/Compiler.thy	Wed Feb 19 22:02:00 2014 +1100
@@ -180,7 +180,7 @@
 "bcomp (Not b) f n = bcomp b (\<not>f) n" |
 "bcomp (And b1 b2) f n =
  (let cb2 = bcomp b2 f n;
-        m = (if f then size cb2 else (size cb2::int)+n);
+        m = if f then size cb2 else (size cb2::int)+n;
       cb1 = bcomp b1 False m
   in cb1 @ cb2)" |
 "bcomp (Less a1 a2) f n =
isabelle