author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 03 May 2010 15:13:15 +0200 | |
changeset 2027 | 68b2d2d7b4ed |
parent 2026 | 7f504136149b |
child 2028 | 15c5a2926622 |
--- 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