# HG changeset patch
# User wenzelm
# Date 1375438675 -7200
# Node ID 820339715ffe79f32ca2dae35837871ad0579d62
# Parent  82ac963c68cbfee0f6502e07d5f2c7c956918b21
tuned proofs;

diff -r 82ac963c68cb -r 820339715ffe src/HOL/MicroJava/DFA/Kildall.thy
--- 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:
diff -r 82ac963c68cb -r 820339715ffe src/HOL/MicroJava/J/Conform.thy
--- 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: 
diff -r 82ac963c68cb -r 820339715ffe src/HOL/MicroJava/J/State.thy
--- 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"