Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proofs;
authorwenzelm
Thu, 01 Mar 2012 14:48:28 +0100
changeset 46742 125e49d04cf6
parent 46741 a29006291f2b
child 46747 b91628b2522b
tuned proofs;
src/HOL/MicroJava/BV/Typing_Framework_JVM.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/Comp/Index.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 01 14:42:05 2012 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 01 14:48:28 2012 +0100
@@ -28,8 +28,8 @@
   "list_all' P xs \<equiv> list_all'_rec P 0 xs"
 
 lemma list_all'_rec:
-  "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
-  apply (induct xs)
+  "list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
+  apply (induct xs arbitrary: n)
   apply auto
   apply (case_tac p)
   apply auto
--- a/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:42:05 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:48:28 2012 +0100
@@ -127,7 +127,7 @@
 lemma wf_java_mdecl_disjoint_varnames: 
   "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) 
   \<Longrightarrow> disjoint_varnames pns lvars"
-apply (case_tac S)
+apply (cases S)
 apply (simp add: wf_java_mdecl_def disjoint_varnames_def  map_of_in_set)
 done
isabelle