--- a/src/HOL/MicroJava/J/Conform.thy Fri Aug 02 11:51:21 2013 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Aug 02 12:17:55 2013 +0200
@@ -137,13 +137,10 @@
apply auto
done
-lemma conf_RefTD [rule_format (no_asm)]:
- "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |
+lemma conf_RefTD [rule_format]:
+ "G,h\<turnstile>a'::\<preceq>RefT T \<Longrightarrow> a' = Null \<or>
(\<exists>a obj T'. a' = Addr a \<and> h a = Some obj \<and> obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
-apply (unfold conf_def)
-apply(induct_tac "a'")
-apply(auto)
-done
+unfolding conf_def by (induct a') auto
lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"
apply (drule conf_RefTD)
@@ -318,7 +315,7 @@
lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |]
==> (x,(h',l))::\<preceq>(G,lT)"
-by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
+by (fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
lemma conforms_upd_obj: