1(*  Author:      Norbert Schirmer
2    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
3    License:     LGPL
4*)
5
6(*  Title:      Simpl.thy
7    Author:     Norbert Schirmer, TU Muenchen
8
9Copyright (C) 2008 Norbert Schirmer
10Some rights reserved, TU Muenchen
11
12This library is free software; you can redistribute it and/or modify
13it under the terms of the GNU Lesser General Public License as
14published by the Free Software Foundation; either version 2.1 of the
15License, or (at your option) any later version.
16
17This library is distributed in the hope that it will be useful, but
18WITHOUT ANY WARRANTY; without even the implied warranty of
19MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
20Lesser General Public License for more details.
21
22You should have received a copy of the GNU Lesser General Public
23License along with this library; if not, write to the Free Software
24Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
25USA
26*)
27(*<*)
28theory Simpl
29imports
30  StateSpace
31  AlternativeSmallStep
32  SyntaxTest
33  "ex/VcgEx"
34  "ex/VcgExSP"
35  "ex/VcgExTotal"
36  "ex/Quicksort"
37  "ex/XVcgEx"
38  "ex/ProcParEx"
39  "ex/ProcParExSP"
40  "ex/ClosureEx"
41  "ex/ComposeEx"
42  UserGuide
43begin
44end
45(*>*)
46