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