| changeset 5184 | 9b8547a9496a |
| parent 4907 | 0eb6730de30f |
| child 7224 | e41e64476f9b |
--- a/src/HOL/Lex/RegExp2NAe.thy Fri Jul 24 13:03:20 1998 +0200 +++ b/src/HOL/Lex/RegExp2NAe.thy Fri Jul 24 13:19:38 1998 +0200 @@ -50,7 +50,7 @@ %s. case s of [] => True | left#s => left & f s)" consts rexp2nae :: 'a rexp => 'a bitsNAe -primrec rexp2nae rexp +primrec "rexp2nae Empty = ([], %a s. {}, %s. False)" "rexp2nae(Atom a) = atom a" "rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"