Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/Abs_Int1_parity.thy
changeset 51711 df3426139651
parent 51625 bd3358aac5d2
child 51826 054a40461449 
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Wed Apr 17 20:53:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Wed Apr 17 21:11:01 2013 +0200
@@ -141,7 +141,7 @@
   ''x'' ::= N 1;
   WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
 
-definition "steps c i = (step_parity(Top(vars c)) ^^ i) (bot c)"
+definition "steps c i = ((step_parity \<top>) ^^ i) (bot c)"
 
 value "show_acom (steps test2_parity 0)"
 value "show_acom (steps test2_parity 1)"
isabelle