src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 33639 603320b93668
parent 33268 02de0317f66f
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:43 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:48 2009 +0100
     1.3 @@ -1233,7 +1233,7 @@
     1.4    also have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
     1.5      using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
     1.6    also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
     1.7 -    by (auto simp add: decr0[OF yes_nb])
     1.8 +    by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
     1.9    also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
    1.10      using qe[rule_format, OF no_qf] by auto
    1.11    finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)"