berghofe [Tue, 24 Apr 2007 15:19:33 +0200] rev 22784
Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe [Tue, 24 Apr 2007 15:18:42 +0200] rev 22783
Added datatype_case.
berghofe [Tue, 24 Apr 2007 15:18:09 +0200] rev 22782
Added intro / elim rules for prod_case.
berghofe [Tue, 24 Apr 2007 15:17:22 +0200] rev 22781
sum_case is now authentic.
berghofe [Tue, 24 Apr 2007 15:15:52 +0200] rev 22780
Adapted to new parse translation for case expressions.
berghofe [Tue, 24 Apr 2007 15:14:31 +0200] rev 22779
Parse / print translations for nested case expressions, taken
from Konrad Slind's TFL package.
berghofe [Tue, 24 Apr 2007 15:13:19 +0200] rev 22778
Streamlined datatype_codegen function using new datatype_of_case
and datatype_of_constr functions.
berghofe [Tue, 24 Apr 2007 15:11:07 +0200] rev 22777
- Moved parse / print translations for case to datatype_case.ML
- Added new functions datatype_of_constr and datatype_of_case
to retrieve datatype corresponding to name of constructor
or case combinator.
berghofe [Tue, 24 Apr 2007 15:07:27 +0200] rev 22776
case constants are now authentic.
narboux [Tue, 24 Apr 2007 14:02:16 +0200] rev 22775
oups : wrong commit
narboux [Tue, 24 Apr 2007 14:01:23 +0200] rev 22774
adds op in front of an infix to fix SML compilation
wenzelm [Mon, 23 Apr 2007 20:44:12 +0200] rev 22773
sane version of read_termTs (proper freeze);
added read_terms, cert_terms;