# HG changeset patch # User wenzelm # Date 1343419076 -7200 # Node ID 6e57023954917569545aa69e21ccbd5eff4f7132 # Parent 7c497a2390070a543343df8bcbef878a31ce1acd# Parent eaa36c0d620ae04740fe3d57f80bb84ce9e957a5 merged diff -r 7c497a239007 -r 6e5702395491 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Jul 27 20:05:56 2012 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Jul 27 21:57:56 2012 +0200 @@ -1051,7 +1051,7 @@ lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simplt t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simplt_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp @@ -1068,7 +1068,7 @@ lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simple t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simple_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp @@ -1085,7 +1085,7 @@ lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simpeq t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simpeq_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp @@ -1102,7 +1102,7 @@ lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simpneq t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simpneq_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp diff -r 7c497a239007 -r 6e5702395491 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Fri Jul 27 20:05:56 2012 +0200 +++ b/src/HOL/GCD.thy Fri Jul 27 21:57:56 2012 +0200 @@ -610,8 +610,8 @@ apply (erule subst) apply (rule iffI) apply force - apply (drule_tac x = "abs e" in exI) - apply (case_tac "e >= 0") + apply (drule_tac x = "abs ?e" in exI) + apply (case_tac "(?e::int) >= 0") apply force apply force done diff -r 7c497a239007 -r 6e5702395491 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Jul 27 20:05:56 2012 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Jul 27 21:57:56 2012 +0200 @@ -132,7 +132,8 @@ in fun beta_of_def thy def_thm = let - val (con, lam) = Logic.dest_equals (concl_of def_thm) + val (con, lam) = + Logic.dest_equals (Logic.unvarify_global (concl_of def_thm)) val (args, rhs) = arglist lam val lhs = list_ccomb (con, args) val goal = mk_equals (lhs, rhs) diff -r 7c497a239007 -r 6e5702395491 src/HOL/HOLCF/ex/Hoare.thy --- a/src/HOL/HOLCF/ex/Hoare.thy Fri Jul 27 20:05:56 2012 +0200 +++ b/src/HOL/HOLCF/ex/Hoare.thy Fri Jul 27 21:57:56 2012 +0200 @@ -267,7 +267,7 @@ lemma hoare_lemma19: "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)" apply (rule flat_codom) -apply (rule_tac t = "x1" in iterate_0 [THEN subst]) +apply (rule_tac t = "x" in iterate_0 [THEN subst]) apply (erule spec) done diff -r 7c497a239007 -r 6e5702395491 src/HOL/MicroJava/Comp/LemmasComp.thy --- a/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jul 27 20:05:56 2012 +0200 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jul 27 21:57:56 2012 +0200 @@ -369,9 +369,6 @@ prefer 2 apply assumption apply (simp add: comp_method [of G D]) apply (erule exE)+ -apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))") -apply (rule exI) -apply (simp) apply (simp add: split_paired_all) apply (intro strip) apply (simp add: comp_method)