author | nipkow |
Tue, 26 Jun 2001 15:28:49 +0200 | |
changeset 11379 | 0c90ffd3f3e2 |
parent 5184 | 9b8547a9496a |
child 12792 | b344226f924c |
permissions | -rw-r--r-- |
(* Title: HOL/Lex/RegExp.thy ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM Regular expressions *) RegExp = RegSet + datatype 'a rexp = Empty | Atom 'a | Union ('a rexp) ('a rexp) | Conc ('a rexp) ('a rexp) | Star ('a rexp) consts lang :: 'a rexp => 'a list set primrec "lang Empty = {}" "lang (Atom a) = {[a]}" "lang (Union el er) = (lang el) Un (lang er)" "lang (Conc el er) = RegSet.conc (lang el) (lang er)" "lang (Star e) = RegSet.star(lang e)" end