changeset 2027 | 68b2d2d7b4ed |
parent 2025 | 070ba8972e97 |
child 2035 | 3622cae9b10e |
--- 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