Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
properly set up the prs_rules
authorChristian Urban <urbanc@in.tum.de>
Tue, 08 Dec 2009 20:34:00 +0100
changeset 643 cd4226736c37
parent 642 005e4edc65ef
child 644 97a397ba5743
properly set up the prs_rules
Quot/QuotMain.thy file | annotate | diff | comparison | revisions
Quot/quotient_info.ML file | annotate | diff | comparison | revisions 
--- 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 {*
--- 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))
nominal2