QuotScript.thy
Fri, 04 Dec 2009 18:32:19 +0100 Cezary Kaliszyk abs_rep as ==
Fri, 04 Dec 2009 17:36:45 +0100 Cezary Kaliszyk Cleaning/review of QuotScript.
Fri, 04 Dec 2009 17:15:55 +0100 Cezary Kaliszyk More cleaning
Fri, 04 Dec 2009 16:53:11 +0100 Cezary Kaliszyk more name cleaning and removing
Fri, 04 Dec 2009 16:40:23 +0100 Cezary Kaliszyk More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
Fri, 04 Dec 2009 16:12:40 +0100 Cezary Kaliszyk Cleaning & Renaming coming from QuotList
Fri, 04 Dec 2009 15:50:57 +0100 Cezary Kaliszyk Even more name changes and cleaning
Fri, 04 Dec 2009 15:41:09 +0100 Cezary Kaliszyk More code cleaning and name changes
Fri, 04 Dec 2009 15:18:37 +0100 Christian Urban smaller theory footprint
Fri, 04 Dec 2009 15:04:05 +0100 Cezary Kaliszyk Naming changes
Fri, 04 Dec 2009 14:35:36 +0100 Cezary Kaliszyk code cleaning and renaming
Fri, 04 Dec 2009 11:33:58 +0100 Cezary Kaliszyk Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
Fri, 04 Dec 2009 10:12:17 +0100 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster.
Fri, 04 Dec 2009 09:33:32 +0100 Cezary Kaliszyk Fixes after big merge.
Fri, 04 Dec 2009 09:18:46 +0100 Cezary Kaliszyk Changing = to \<equiv> in case if we want to use simp.
less more (0) -15 tip