src/HOL/Bali/Example.thy
changeset 36319 8feb2c4bef1a
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/Example.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -1070,7 +1070,7 @@
     1.4  
     1.5  section "well-typedness"
     1.6  
     1.7 -lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
     1.8 +schematic_lemma 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 @@ -1122,7 +1122,7 @@
    1.13  
    1.14  section "definite assignment"
    1.15  
    1.16 -lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
    1.17 +schematic_lemma 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 @@ -1241,7 +1241,7 @@
    1.22  
    1.23  
    1.24  declare Pair_eq [simp del]
    1.25 -lemma exec_test: 
    1.26 +schematic_lemma 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>