1.1 --- a/src/HOL/Bali/Example.thy	Tue Oct 06 13:31:44 2015 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Tue Oct 06 15:14:28 2015 +0200
     1.3 @@ -1078,7 +1078,7 @@
     1.4  
     1.5  subsubsection "well-typedness"
     1.6  
     1.7 -schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
     1.8 +schematic_goal wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
     1.9  apply (unfold test_def arr_viewed_from_def)
    1.10  (* ?pTs = [Class Base] *)
    1.11  apply (rule wtIs (* ;; *))
    1.12 @@ -1130,7 +1130,7 @@
    1.13  
    1.14  subsubsection "definite assignment"
    1.15  
    1.16 -schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
    1.17 +schematic_goal da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
    1.18                    \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
    1.19  apply (unfold test_def arr_viewed_from_def)
    1.20  apply (rule da.Comp)
    1.21 @@ -1248,7 +1248,7 @@
    1.22  
    1.23  
    1.24  declare Pair_eq [simp del]
    1.25 -schematic_lemma exec_test: 
    1.26 +schematic_goal exec_test: 
    1.27  "\<lbrakk>the (new_Addr (heap  s1)) = a;  
    1.28    the (new_Addr (heap ?s2)) = b;  
    1.29    the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>