src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 48562 f6d6d58fa318 parent 47108 2a1953f0d20d child 49962 a8cc904a6820
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Jul 27 19:27:21 2012 +0200
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Jul 27 19:57:23 2012 +0200
1.3 @@ -1051,7 +1051,7 @@
1.4
1.5  lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.6    shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
1.7 -  using split0 [of "simptm t" vs bs]
1.8 +  using split0 [of "simptm t" "vs::'a list" bs]
1.9  proof(simp add: simplt_def Let_def split_def)
1.10    assume nb: "tmbound0 t"
1.11    hence nb': "tmbound0 (simptm t)" by simp
1.12 @@ -1068,7 +1068,7 @@
1.13
1.14  lemma simple_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.15    shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
1.16 -  using split0 [of "simptm t" vs bs]
1.17 +  using split0 [of "simptm t" "vs::'a list" bs]
1.18  proof(simp add: simple_def Let_def split_def)
1.19    assume nb: "tmbound0 t"
1.20    hence nb': "tmbound0 (simptm t)" by simp
1.21 @@ -1085,7 +1085,7 @@
1.22
1.23  lemma simpeq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.24    shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
1.25 -  using split0 [of "simptm t" vs bs]
1.26 +  using split0 [of "simptm t" "vs::'a list" bs]
1.27  proof(simp add: simpeq_def Let_def split_def)
1.28    assume nb: "tmbound0 t"
1.29    hence nb': "tmbound0 (simptm t)" by simp
1.30 @@ -1102,7 +1102,7 @@
1.31
1.32  lemma simpneq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.33    shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
1.34 -  using split0 [of "simptm t" vs bs]
1.35 +  using split0 [of "simptm t" "vs::'a list" bs]
1.36  proof(simp add: simpneq_def Let_def split_def)
1.37    assume nb: "tmbound0 t"
1.38    hence nb': "tmbound0 (simptm t)" by simp
```