author | paulson |
Wed, 25 Jul 2001 13:13:01 +0200 | |
changeset 11451 | 8abfb4f7bd02 |
parent 8732 | aef229ca5e77 |
child 14431 | ade3d26e0caf |
permissions | -rw-r--r-- |
(* Title: HOL/Lex/RegSet.thy ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM Regular sets *) RegSet = Main + constdefs conc :: 'a list set => 'a list set => 'a list set "conc A B == {xs@ys | xs ys. xs:A & ys:B}" consts star :: 'a list set => 'a list set inductive "star A" intrs NilI "[] : star A" ConsI "[| a:A; as : star A |] ==> a@as : star A" end