changeset 5184 | 9b8547a9496a |
parent 4832 | bc11b5b06f87 |
child 11379 | 0c90ffd3f3e2 |
--- a/src/HOL/Lex/RegExp.thy Fri Jul 24 13:03:20 1998 +0200 +++ b/src/HOL/Lex/RegExp.thy Fri Jul 24 13:19:38 1998 +0200 @@ -15,7 +15,7 @@ | Star ('a rexp) consts lang :: 'a rexp => 'a list set -primrec lang rexp +primrec lang_Emp "lang Empty = {}" lang_Atom "lang (Atom a) = {[a]}" lang_Un "lang (Union el er) = (lang el) Un (lang er)"