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.
merged
authorwenzelm
Thu, 18 Oct 2012 15:44:14 +0200
changeset 49925 18af317f393a
parent 49920 26a0263f9f46 (diff)
parent 49924 12cece6d951d (current diff)
child 49926 a9f5a7496258
merged
--- a/src/HOL/IMP/BExp.thy	Thu Oct 18 15:28:49 2012 +0200
+++ b/src/HOL/IMP/BExp.thy	Thu Oct 18 15:44:14 2012 +0200
@@ -80,7 +80,7 @@
 
 value "bsimp (And (Less (N 0) (N 1)) b)"
 
-value "bsimp (And (Less (N 1) (N 0)) (B True))"
+value "bsimp (And (Less (N 1) (N 0)) (Bc True))"
 
 theorem "bval (bsimp b) s = bval b s"
 apply(induction b)
isabelle