--- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Apr 29 13:40:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Apr 29 13:41:34 2013 +0200
@@ -572,7 +572,6 @@
val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]}
else @{thm ordLeq_csum2[OF Card_order_ctwo]};
val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp});
- val Asuc_bd_Cnotzero = Asuc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
[suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
@@ -671,7 +670,7 @@
(K (mk_min_algs_card_of_tac card_cT card_ct
m suc_bd_worel min_algs_thms in_bd_sums
sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
- suc_bd_Asuc_bd Asuc_bd_Cinfinite Asuc_bd_Cnotzero)))
+ suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
|> Thm.close_derivation;
val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Mon Apr 29 13:40:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Mon Apr 29 13:41:34 2013 +0200
@@ -47,7 +47,7 @@
val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
- thm -> thm -> thm -> thm -> thm -> thm -> tactic
+ thm -> thm -> thm -> thm -> thm -> tactic
val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
val mk_min_algs_tac: thm -> thm list -> tactic
@@ -286,7 +286,7 @@
rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
- suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite Asuc_Cnotzero =
+ suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
let
val induct = worel RS
Drule.instantiate' [SOME cT] [NONE, SOME ct] @{thm well_order_induct_imp};