# HG changeset patch # User wenzelm # Date 1330609708 -3600 # Node ID 125e49d04cf6cccdf615f474b4a7102d90901989 # Parent a29006291f2bd16c44307a382bffb9301db33a76 tuned proofs; diff -r a29006291f2b -r 125e49d04cf6 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy --- 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 \ list_all'_rec P 0 xs" lemma list_all'_rec: - "\n. list_all'_rec P n xs = (\p < size xs. P (xs!p) (p+n))" - apply (induct xs) + "list_all'_rec P n xs = (\p < size xs. P (xs!p) (p+n))" + apply (induct xs arbitrary: n) apply auto apply (case_tac p) apply auto diff -r a29006291f2b -r 125e49d04cf6 src/HOL/MicroJava/Comp/Index.thy --- 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)) \ 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