Fri, 04 Dec 2009 15:20:06 +0100 merged
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 15:20:06 +0100] rev 532
merged
Fri, 04 Dec 2009 15:19:39 +0100 merge
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 15:19:39 +0100] rev 531
merge
Fri, 04 Dec 2009 15:18:37 +0100 smaller theory footprint
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 15:18:37 +0100] rev 530
smaller theory footprint
Fri, 04 Dec 2009 15:18:33 +0100 More name changes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:18:33 +0100] rev 529
More name changes
Fri, 04 Dec 2009 15:04:05 +0100 Naming changes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 15:04:05 +0100] rev 528
Naming changes
Fri, 04 Dec 2009 14:35:36 +0100 code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:35:36 +0100] rev 527
code cleaning and renaming
Fri, 04 Dec 2009 14:11:20 +0100 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:11:20 +0100] rev 526
merge
Fri, 04 Dec 2009 14:11:03 +0100 Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 14:11:03 +0100] rev 525
Removed previous inj_repabs_tac
Fri, 04 Dec 2009 13:58:23 +0100 some tuning
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 13:58:23 +0100] rev 524
some tuning
Fri, 04 Dec 2009 12:21:15 +0100 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 04 Dec 2009 12:21:15 +0100] rev 523
merge
Fri, 04 Dec 2009 12:20:49 +0100 rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
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.
Fri, 04 Dec 2009 11:34:49 +0100 merged
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 11:34:49 +0100] rev 521
merged
Fri, 04 Dec 2009 11:34:21 +0100 merged
Christian Urban <urbanc@in.tum.de> [Fri, 04 Dec 2009 11:34:21 +0100] rev 520
merged
Fri, 04 Dec 2009 11:33:58 +0100 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: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.
Fri, 04 Dec 2009 11:06:43 +0100 compose_tac instead of rtac to avoid unification; some code cleaning.
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.
(0) -300 -100 -15 +15 +100 +300 +1000 tip