--- a/src/HOL/Bali/Example.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Bali/Example.thy Tue Oct 06 15:14:28 2015 +0200
@@ -1078,7 +1078,7 @@
subsubsection "well-typedness"
-schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
+schematic_goal wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
apply (unfold test_def arr_viewed_from_def)
(* ?pTs = [Class Base] *)
apply (rule wtIs (* ;; *))
@@ -1130,7 +1130,7 @@
subsubsection "definite assignment"
-schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
+schematic_goal da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
\<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
apply (unfold test_def arr_viewed_from_def)
apply (rule da.Comp)
@@ -1248,7 +1248,7 @@
declare Pair_eq [simp del]
-schematic_lemma exec_test:
+schematic_goal exec_test:
"\<lbrakk>the (new_Addr (heap s1)) = a;
the (new_Addr (heap ?s2)) = b;
the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>