Sat, 05 Dec 2009 23:35:09 +0100 |
Cezary Kaliszyk |
Used symmetric definitions. Moved quotient_rsp to QuotMain.
|
file |
diff |
annotate
|
Sat, 05 Dec 2009 23:26:08 +0100 |
Cezary Kaliszyk |
Proved foldl_rsp and ho_map_rsp
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 16:53:11 +0100 |
Cezary Kaliszyk |
more name cleaning and removing
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 16:40:23 +0100 |
Cezary Kaliszyk |
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 16:12:40 +0100 |
Cezary Kaliszyk |
Cleaning & Renaming coming from QuotList
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 15:50:57 +0100 |
Cezary Kaliszyk |
Even more name changes and cleaning
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 15:23:10 +0100 |
Christian Urban |
smaller theory footprint
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 15:18:33 +0100 |
Cezary Kaliszyk |
More name changes
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 09:33:32 +0100 |
Cezary Kaliszyk |
Fixes after big merge.
|
file |
diff |
annotate
|
Fri, 04 Dec 2009 09:18:46 +0100 |
Cezary Kaliszyk |
Changing = to \<equiv> in case if we want to use simp.
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 22:35:48 +0200 |
Christian Urban |
used new cong_tac
|
file |
diff |
annotate
|
Tue, 11 Aug 2009 12:29:15 +0200 |
Christian Urban |
initial commit
|
file |
diff |
annotate
|