changeset 2314 | 1a14c4171a51 |
parent 2313 | 25d2cdf7d7e4 |
child 2316 | 08bbde090a17 |
--- a/Nominal/NewParser.thy Wed Jun 09 15:14:16 2010 +0200 +++ b/Nominal/NewParser.thy Thu Jun 10 14:53:28 2010 +0200 @@ -5,6 +5,11 @@ "Perm" "Tacs" "Equivp" "Lift" begin +(* TODO + + we need to also export a cases-rule for nominal datatypes + size function +*) section{* Interface for nominal_datatype *}