Mon, 07 Dec 2009 21:53:50 +0100 removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Christian Urban <urbanc@in.tum.de> [Mon, 07 Dec 2009 21:53:50 +0100] rev 610
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
Mon, 07 Dec 2009 21:25:49 +0100 3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 07 Dec 2009 21:25:49 +0100] rev 609
3 lambda examples in FSet. In the last one regularize_term fails.
Mon, 07 Dec 2009 21:21:57 +0100 Handling of errors in lambda_prs_conv.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 07 Dec 2009 21:21:57 +0100] rev 608
Handling of errors in lambda_prs_conv.
Mon, 07 Dec 2009 21:21:23 +0100 babs_prs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 07 Dec 2009 21:21:23 +0100] rev 607
babs_prs
Mon, 07 Dec 2009 18:49:14 +0100 clarified the function examples
Christian Urban <urbanc@in.tum.de> [Mon, 07 Dec 2009 18:49:14 +0100] rev 606
clarified the function examples
Mon, 07 Dec 2009 17:57:33 +0100 first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de> [Mon, 07 Dec 2009 17:57:33 +0100] rev 605
first attempt to deal with Babs in regularise and cleaning (not yet working)
Mon, 07 Dec 2009 15:21:51 +0100 isabelle make tests all examples
Christian Urban <urbanc@in.tum.de> [Mon, 07 Dec 2009 15:21:51 +0100] rev 604
isabelle make tests all examples
Mon, 07 Dec 2009 15:18:44 +0100 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 07 Dec 2009 15:18:44 +0100] rev 603
merge
Mon, 07 Dec 2009 15:18:00 +0100 make_inst for lambda_prs where the second quotient is not identity.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 07 Dec 2009 15:18:00 +0100] rev 602
make_inst for lambda_prs where the second quotient is not identity.
Mon, 07 Dec 2009 14:37:10 +0100 added "end" to each example theory
Christian Urban <urbanc@in.tum.de> [Mon, 07 Dec 2009 14:37:10 +0100] rev 601
added "end" to each example theory
(0) -300 -100 -10 +10 +100 +300 +1000 tip