src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 55422 6445a05a1234 parent 55417 01fbfb60c33e child 55754 d14072d53c1e
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:37:28 2014 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:37:28 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 x1", auto)
1.8 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", 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 x1", auto)
1.14 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
1.15
1.16  fun disjuncts :: "fm \<Rightarrow> fm list" where
1.17    "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
```