# HG changeset patch # User wenzelm # Date 1326543759 -3600 # Node ID d3d62b528487293d6ff230911f21b60b5e35f430 # Parent 07e334ad2e2a1aa79300f99f8893902dc815a583 tuned proofs; diff -r 07e334ad2e2a -r d3d62b528487 src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Sat Jan 14 13:11:32 2012 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Sat Jan 14 13:22:39 2012 +0100 @@ -328,9 +328,7 @@ apply auto apply(rule hconfI) apply(drule conforms_heapD) -apply(tactic {* - auto_tac (put_claset HOL_cs @{context} addEs [@{thm oconf_hext}] addDs [@{thm hconfD}] - |> map_simpset (fn ss => ss delsimps [@{thm split_paired_All}])) *}) +apply(auto elim: oconf_hext dest: hconfD) done lemma conforms_upd_local: diff -r 07e334ad2e2a -r d3d62b528487 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Sat Jan 14 13:11:32 2012 +0100 +++ b/src/HOL/Unix/Unix.thy Sat Jan 14 13:22:39 2012 +0100 @@ -1034,7 +1034,7 @@ lookup root ((path @ [y]) @ us) \ None" by cases (auto dest: access_some_lookup) then show ?thesis - by (simp, blast dest!: lookup_some_append) + by (fastforce dest!: lookup_some_append) qed finally show ?thesis . qed