src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 55417 01fbfb60c33e parent 54742 7a86358a3c0b child 55422 6445a05a1234
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:35:57 2014 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:37:06 2014 +0100
1.3 @@ -761,12 +761,12 @@
1.4  lemma evaldjf_bound0:
1.5    assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
1.6    shows "bound0 (evaldjf f xs)"
1.7 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
1.8 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
1.9
1.10  lemma evaldjf_qf:
1.11    assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
1.12    shows "qfree (evaldjf f xs)"
1.13 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
1.14 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
1.15
1.16  fun disjuncts :: "fm \<Rightarrow> fm list" where
1.17    "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
1.18 @@ -3003,5 +3003,3 @@
1.19  oops
1.20  *)
1.21  end
1.22 -
1.23 -
```