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 -