Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/Typing_Framework_err.thy
changeset 32417 e87d9c78910c
parent 27680 5a557a5afc48 
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Aug 26 19:54:19 2009 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Thu Aug 27 09:28:52 2009 +0200
@@ -62,15 +62,9 @@
 lemma bounded_err_stepI:
   "\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
   \<Longrightarrow> bounded (err_step n ap step) n"
-apply (unfold bounded_def)
-apply clarify
-apply (simp add: err_step_def split: err.splits)
-apply (simp add: error_def)
- apply blast
-apply (simp split: split_if_asm) 
- apply (blast dest: in_map_sndD)
-apply (simp add: error_def)
-apply blast
+apply (clarsimp simp: bounded_def err_step_def split: err.splits)
+apply (simp add: error_def image_def)
+apply (blast dest: in_map_sndD)
 done
isabelle