--- a/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 02 11:51:21 2013 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Fri Aug 02 12:17:55 2013 +0200
@@ -67,9 +67,8 @@
(** merges **)
-lemma length_merges [rule_format, simp]:
- "\<forall>ss. size(merges f ps ss) = size ss"
- by (induct_tac ps, auto)
+lemma length_merges [simp]: "size(merges f ps ss) = size ss"
+ by (induct ps arbitrary: ss) auto
lemma (in Semilat) merges_preserves_type_lemma:
--- 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:
--- a/src/HOL/MicroJava/J/State.thy Fri Aug 02 11:51:21 2013 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Aug 02 12:17:55 2013 +0200
@@ -105,10 +105,7 @@
lemma raise_if_Some2 [simp]:
"raise_if c z (if x = None then Some y else x) \<noteq> None"
-apply (unfold raise_if_def)
-apply(induct_tac "x")
-apply auto
-done
+unfolding raise_if_def by (induct x) auto
lemma raise_if_SomeD [rule_format (no_asm)]:
"raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some (Addr (XcptRef x)) | y = Some z"