# HG changeset patch
# User nipkow
# Date 1047391464 -3600
# Node ID f5d08c341216aa1af328317cee13045f25f82321
# Parent  644692eca537830eb1bee3e8cb03e83c1eb91758
*** empty log message ***

diff -r 644692eca537 -r f5d08c341216 src/HOL/Hoare/ExamplesAbort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 11 15:04:24 2003 +0100
@@ -0,0 +1,23 @@
+theory ExamplesAbort = HoareAbort:
+
+syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("_ \<rightarrow> _" 60)
+translations "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
+
+lemma "VARS x y z::nat
+ {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
+by vcg_simp
+
+lemma "VARS (a::int list) i
+ {True}
+ i := 0;
+ WHILE i < length a
+ INV {i <= length a}
+ DO i < length a \<rightarrow> a := a[i := 7];
+    i := i+1
+ OD
+ {True}"
+apply vcg_simp
+apply arith
+done
+
+end