src/HOL/MicroJava/J/Example.thy
changeset 36319 8feb2c4bef1a
parent 35102 cc7a0b9f938c
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/MicroJava/J/Example.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Example.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4  done
     1.5  
     1.6  ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
     1.7 -lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
     1.8 +schematic_lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
     1.9    Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
    1.10  apply (tactic t) -- ";;"
    1.11  apply  (tactic t) -- "Expr"
    1.12 @@ -400,7 +400,7 @@
    1.13  
    1.14  declare split_if [split del]
    1.15  declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
    1.16 -lemma exec_test: 
    1.17 +schematic_lemma exec_test: 
    1.18  " [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
    1.19    tprg\<turnstile>s0 -test-> ?s"
    1.20  apply (unfold test_def)