Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/QuotMain.thy
changeset 643 cd4226736c37
parent 642 005e4edc65ef
child 648 830b58c2fa94 
--- 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 {*
nominal2