src/HOL/Nominal/nominal_atoms.ML
changeset 24569 c80e1871098b
parent 24527 888d56a8d9d3
child 24677 c6295d2dce48
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Sep 13 18:06:50 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Sep 13 18:08:08 2007 +0200
     1.3 @@ -21,6 +21,8 @@
     1.4  val finite_emptyI = @{thm "finite.emptyI"};
     1.5  val Collect_const = @{thm "Collect_const"};
     1.6  
     1.7 +val inductive_forall_def = @{thm "induct_forall_def"};
     1.8 +
     1.9  
    1.10  (* theory data *)
    1.11  
    1.12 @@ -803,7 +805,13 @@
    1.13              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    1.14              ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
    1.15              ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
    1.16 -            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_force_add])] 
    1.17 +            ||>> PureThy.add_thmss
    1.18 +              let
    1.19 +                val thms1 = inst_pt_at [all_eqvt];
    1.20 +                val thms2 = map (fold_rule [inductive_forall_def]) thms1
    1.21 +              in
    1.22 +                [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
    1.23 +              end
    1.24              ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
    1.25              ||>> PureThy.add_thmss 
    1.26  	      let val thms1 = inst_at [at_fresh]