# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261953190 -3600
# Node ID 35436401f00d827050b9fa5906644943fa2b6973
# Parent  64f9c76f70c7ec3f7d97ef7a80cf0737744ccb6a
added a functor that allows checking what is added to the theorem lists

diff -r 64f9c76f70c7 -r 35436401f00d Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Dec 26 23:20:46 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sun Dec 27 23:33:10 2009 +0100
@@ -234,16 +234,17 @@
 (* type variables ?'a1.0 (which are turned into frees *)
 (* 'a_1                                               *)
 lemma concat1: 
-  shows "concat [] = []"
+  shows "concat [] \<approx> []"
 by (simp)
 
 lemma concat2: 
-  shows "concat (x # xs) =  x @ concat xs"
+  shows "concat (x # xs) \<approx>  x @ concat xs"
 by (simp)
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-apply(lifting concat1)
+apply(lifting_setup concat1)
+apply(regularize)
 apply(injection)
 defer
 apply(cleaning)
diff -r 64f9c76f70c7 -r 35436401f00d Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Sat Dec 26 23:20:46 2009 +0100
+++ b/Quot/quotient_info.ML	Sun Dec 27 23:33:10 2009 +0100
@@ -32,6 +32,34 @@
   val quotient_rules_add: attribute
 end;
 
+functor Named_Thms_Ext (val name: string val description: string val filter: thm -> thm): NAMED_THMS =
+struct
+
+structure Data = Generic_Data
+(
+  type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
+  val extend = I;
+  val merge = Item_Net.merge;
+);
+
+val content = Item_Net.content o Data.get;
+val get = content o Context.Proof;
+
+val add_thm = Data.map o Item_Net.update o filter;
+val del_thm = Data.map o Item_Net.remove;
+
+val add = Thm.declaration_attribute add_thm;
+val del = Thm.declaration_attribute del_thm;
+
+val setup =
+  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
+  PureThy.add_thms_dynamic (Binding.name name, content);
+
+end;
+
+
+
 structure Quotient_Info: QUOTIENT_INFO =
 struct
 
@@ -216,9 +244,10 @@
 val equiv_rules_add = EquivRules.add
 
 (* respectfulness theorems *)
-structure RspRules = Named_Thms
+structure RspRules = Named_Thms_Ext
   (val name = "quot_respect"
-   val description = "Respectfulness theorems.")
+   val description = "Respectfulness theorems."
+   val filter = fn x => x)
 
 val rsp_rules_get = RspRules.get
 
diff -r 64f9c76f70c7 -r 35436401f00d Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Dec 26 23:20:46 2009 +0100
+++ b/Quot/quotient_term.ML	Sun Dec 27 23:33:10 2009 +0100
@@ -402,6 +402,7 @@
   regularize_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
 
+
 (*********************)
 (* Rep/Abs Injection *)
 (*********************)
@@ -430,7 +431,7 @@
 
   For free variables:
 
-  * We put aRep/Abs around it if the type needs lifting.
+  * We put a Rep/Abs around it if the type needs lifting.
 
   Vars case cannot occur.
 *)