# HG changeset patch
# User urbanc
# Date 1130925749 -3600
# Node ID 2493cb9f5ede4b3adfbd58c5dc515272ce07a357
# Parent  2719a6b7d95e6ee33ffbafe512e27e98f651ec43
added the collection of lemmas "supp_at"

diff -r 2719a6b7d95e -r 2493cb9f5ede src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Nov 01 23:55:53 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 11:02:29 2005 +0100
@@ -770,6 +770,10 @@
        val pt_bij            = PureThy.get_thm thy32 (Name ("nominal.pt_bij"));
        val pt_perm_compose   = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose"));
        val perm_eq_app       = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app"));
+       val at_fresh          = PureThy.get_thm thy32 (Name ("nominal.at_fresh"));
+       (*val at_calc           = PureThy.get_thms thy32 (Name ("nominal.at_calc"));*)
+       val at_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
+       val dj_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
 
        (* abs_perm collects all lemmas for simplifying a permutation *)
        (* in front of an abs_fun                                     *)
@@ -792,31 +796,21 @@
              (PureThy.add_thmss [((name, thm_list),[])] thy32)
            end;
 
-        (* alpha collects all lemmas analysing an equation *)
-        (* between abs_funs                                *)
-        (*val (thy34,_) = 
+       val (thy34,_) = 
 	   let 
-	     val name = "alpha"
-             val thm_list = map (fn (ak_name, T) =>
-	        let	
-		  val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
-		  val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
-	        in
-                  [pt_inst, at_inst] MRS abs_fun_eq
-	        end) ak_names_types
-           in
-             (PureThy.add_thmss [((name, thm_list),[])] thy33)
-           end;*)
- 
-          val (thy34,_) = 
-	   let 
-	     fun inst_pt_at thm ak_name =
+	       fun inst_pt_at thm ak_name =
 		 let	
 		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
 		   val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
 	         in
                      [pt_inst, at_inst] MRS thm
-	         end	 
+	         end	
+               fun inst_at thm ak_name =
+		 let	
+		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
+                 in
+                     at_inst RS thm
+	         end
 
            in
             thy33 
@@ -826,6 +820,11 @@
             |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]
             |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]
             |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]
+            |>>> PureThy.add_thmss [(("supp_at", map (inst_at at_supp) ak_names),[])]
+            (*|>>> PureThy.add_thmss [(("fresh_at", map (inst_at at_fresh) ak_names),
+                                    [Simplifier.simp_add_global])]*)
+            (*|>>> PureThy.add_thmss [(("calc_at", map (inst_at at_calc) ak_names),
+                                    [Simplifier.simp_add_global])]*)
 	   end;
 
          (* perm_dj collects all lemmas that forget an permutation *)