rolled back the last addition since these lemmas were already
authorurbanc
Wed Jan 11 12:21:01 2006 +0100 (2006-01-11)
changeset 186523930a060d71b
parent 18651 0cb5a8f501aa
child 18653 7a00c80400b1
rolled back the last addition since these lemmas were already
in the simpset.
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 11 12:14:25 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 11 12:21:01 2006 +0100
     1.3 @@ -714,7 +714,6 @@
     1.4  	       in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
     1.5               (* list of all fs_inst-theorems *)
     1.6               val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
     1.7 -             val pt_id = map (fn ak => PureThy.get_thm thy32 (Name ("pt_"^ak^"1"))) ak_names
     1.8                
     1.9               fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms); 
    1.10               fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);               
    1.11 @@ -731,8 +730,7 @@
    1.12               fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
    1.13             in
    1.14              thy32 
    1.15 -	    |>   PureThy.add_thmss [(("pt_id", pt_id),[])]
    1.16 -            ||>> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.17 +	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.18              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
    1.19              ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
    1.20              ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]