# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260300840 -3600
# Node ID cd4226736c3716a00c3bb1017081c870bf72a59d
# Parent  005e4edc65ef5ea5bbf56daf3cecb04d206f9487
properly set up the prs_rules

diff -r 005e4edc65ef -r cd4226736c37 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 17:43:32 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 20:34:00 2009 +0100
@@ -1043,10 +1043,11 @@
 (* 1. conversion (is not a pattern) *)
 thm lambda_prs
 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
+(*    prservation lemma                                           *)
 (*    and simplification with                                     *)
 thm all_prs ex_prs 
 (* 3. simplification with *)
-thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps
+thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps 
 (* 4. Test for refl *)
 
 ML {*
diff -r 005e4edc65ef -r cd4226736c37 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Dec 08 17:43:32 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 08 20:34:00 2009 +0100
@@ -220,6 +220,7 @@
 val _ = Context.>> (Context.map_theory 
     (EquivRules.setup #>
      RspRules.setup #>
+     PrsRules.setup #>
      IdSimps.setup #>
      QuotientRules.setup))