author wenzelm Fri, 27 Jul 2012 21:57:56 +0200 changeset 48566 6e5702395491 parent 48565 7c497a239007 (current diff) parent 48564 eaa36c0d620a (diff) child 48567 3c4d7ff75f01 child 48568 084cd758a8ab
merged
```--- 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 \<Longrightarrow> bound0 (simplt t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
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 \<Longrightarrow> bound0 (simple t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
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 \<Longrightarrow> bound0 (simpeq t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
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 \<Longrightarrow> bound0 (simpneq t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
assume nb: "tmbound0 t"
hence nb': "tmbound0 (simptm t)" by simp```
```--- 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```
```--- 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)```
```--- 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
```
```--- 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)