Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 16:53:11 +0100] rev 541
more name cleaning and removing
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 16:40:23 +0100] rev 540
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 16:12:40 +0100] rev 539
Cleaning & Renaming coming from QuotList
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 16:01:23 +0100] rev 538
Cleaning in Quotients
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:50:57 +0100] rev 537
Even more name changes and cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:41:09 +0100] rev 536
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:25:51 +0100] rev 535
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:25:26 +0100] rev 534
merged
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 15:23:10 +0100] rev 533
smaller theory footprint
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 15:20:06 +0100] rev 532
merged
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 15:19:39 +0100] rev 531
merge
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 15:18:37 +0100] rev 530
smaller theory footprint
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:18:33 +0100] rev 529
More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:04:05 +0100] rev 528
Naming changes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:35:36 +0100] rev 527
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:11:20 +0100] rev 526
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:11:03 +0100] rev 525
Removed previous inj_repabs_tac
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 13:58:23 +0100] rev 524
some tuning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 12:21:15 +0100] rev 523
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 12:20:49 +0100] rev 522
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 11:34:49 +0100] rev 521
merged
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 11:34:21 +0100] rev 520
merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 11:33:58 +0100] rev 519
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 11:06:43 +0100] rev 518
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 10:36:35 +0100] rev 517
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 10:12:17 +0100] rev 516
Using APPLY_RSP1; again a little bit faster.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 09:33:32 +0100] rev 515
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 09:25:27 +0100] rev 514
The big merge; probably non-functional.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 09:08:51 +0100] rev 513
Testing the new tactic everywhere
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 09:01:13 +0100] rev 512
First version of the deterministic rep-abs-inj-tac.