src/HOL/Nominal/nominal_atoms.ML
changeset 22715 381e6c45f13b
parent 22611 0e008e3ddb1e
child 22745 17bc6af2011e
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 16 06:45:22 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 16 07:32:23 2007 +0200
     1.3 @@ -802,8 +802,8 @@
     1.4              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
     1.5              ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
     1.6              ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
     1.7 -            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])] 
     1.8 -            ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
     1.9 +            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_force_add])] 
    1.10 +            ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
    1.11              ||>> PureThy.add_thmss 
    1.12  	      let val thms1 = inst_at [at_fresh]
    1.13  		  val thms2 = inst_dj [at_fresh_ineq]