Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 27 Jan 2010 12:21:40 +0100] rev 960
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 27 Jan 2010 12:19:58 +0100] rev 959
When commenting discovered a missing case of Babs->Abs regularization.
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 12:19:21 +0100] rev 958
merged
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 12:19:00 +0100] rev 957
mostly ported Terms.thy to new Nominal
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 27 Jan 2010 12:06:43 +0100] rev 956
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 27 Jan 2010 12:06:24 +0100] rev 955
Commenting regularize
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 11:48:04 +0100] rev 954
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 11:31:16 +0100] rev 953
reordered cases in regularize (will be merged into two cases)
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 08:41:42 +0100] rev 952
use of equiv_relation_chk in quotient_term
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 08:20:31 +0100] rev 951
some slight tuning
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 07:49:43 +0100] rev 950
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de> [Wed, 27 Jan 2010 07:45:01 +0100] rev 949
added another example with indirect recursion over lists