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/AbsInt0_const.thy
changeset 44944 f136409c2cef
parent 44932 7c93ee993cae 
--- a/src/HOL/IMP/AbsInt0_const.thy	Sat Sep 17 03:37:14 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_const.thy	Sat Sep 17 04:41:44 2011 +0200
@@ -61,10 +61,10 @@
     by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
 qed
 
-interpretation Abs_Int rep_cval Const plus_cval "(iter_above 3)"
+interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
 defines AI_const is AI
 and aval'_const is aval'
-proof qed (auto simp: iter_above_pfp)
+proof qed (auto simp: iter'_pfp_above)
 
 text{* Straight line code: *}
 definition "test1_const =
isabelle