Comment
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 03 May 2010 15:13:15 +0200
changeset 2027 68b2d2d7b4ed
parent 2026 7f504136149b
child 2028 15c5a2926622
Comment
Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 03 14:31:11 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 15:13:15 2010 +0200
@@ -159,8 +159,9 @@
 end
 *}
 
-text {* What does the prep_bn code do? Cezary's Function? *}
-
+(* strip_bn_fun takes a bn function defined by the user as a union or
+   append of elements and returns those elements together with bn functions
+   applied *)
 ML {*
 fun strip_bn_fun t =
   case t of