Nominal/NewParser.thy
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 *}