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/MicroJava/J/JListExample.thy
changeset 68451 c34aa23a1fb6
parent 63176 878bd5922f3b 
--- a/src/HOL/MicroJava/J/JListExample.thy	Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Jun 15 13:02:12 2018 +0200
@@ -162,10 +162,10 @@
          append_name({[RefT (ClassT list_name)]}[LAcc l4_name]))"
 
 definition test where
-  "test = Predicate.Pred (\<lambda>s. example_prg\<turnstile>Norm (empty, empty) -E-> s)"
+  "test = Predicate.Pred (\<lambda>s. example_prg\<turnstile>Norm (Map.empty, Map.empty) -E-> s)"
 
 lemma test_code [code]:
-  "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
+  "test = exec_i_i_i_o example_prg (Norm (Map.empty, Map.empty)) E"
 by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
 
 ML_val \<open>
isabelle