changeset 13857 | 11d7c5a8dbb7 |
parent 13856 | f5d08c341216 |
child 13875 | 12997e3ddd8d |
--- a/src/HOL/Hoare/ExamplesAbort.thy Tue Mar 11 15:04:24 2003 +0100 +++ b/src/HOL/Hoare/ExamplesAbort.thy Tue Mar 11 15:04:24 2003 +0100 @@ -1,3 +1,12 @@ +(* Title: HOL/Hoare/ExamplesAbort.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1998 TUM + +Some small examples for programs that may abort. +Currently only show the absence of abort. +*) + theory ExamplesAbort = HoareAbort: syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("_ \<rightarrow> _" 60)