# HG changeset patch
# User nipkow
# Date 817062536 -3600
# Node ID 7bdc4699ef4d7fcab01f6c41c45565a3b6ef2bfc
# Parent  5fdd4da11d4908711d48965dbe8953fb80a24788
Added List_Examples

diff -r 5fdd4da11d49 -r 7bdc4699ef4d src/HOL/Hoare/List_Examples.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/List_Examples.ML	Wed Nov 22 18:48:56 1995 +0100
@@ -0,0 +1,29 @@
+goal thy
+"{x=X} \
+\ y := []; \
+\ WHILE x ~= [] \
+\ DO { rev(x)@y = rev(X)} \
+\    y := hd x # y; x := tl x \
+\ END \
+\{y=rev(X)}";
+by(hoare_tac 1);
+by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
+by(safe_tac HOL_cs);
+by(Asm_full_simp_tac 1);
+by(Asm_full_simp_tac 1);
+qed "imperative_reverse";
+
+goal thy
+"{x=X & y = Y} \
+\ x := rev(x); \
+\ WHILE x ~= [] \
+\ DO { rev(x)@y = X@Y} \
+\    y := hd x # y; x := tl x \
+\ END \
+\{y = X@Y}";
+by(hoare_tac 1);
+by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
+by(safe_tac HOL_cs);
+by(Asm_full_simp_tac 1);
+by(Asm_full_simp_tac 1);
+qed "imperative_append";
diff -r 5fdd4da11d49 -r 7bdc4699ef4d src/HOL/Hoare/List_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/List_Examples.thy	Wed Nov 22 18:48:56 1995 +0100
@@ -0,0 +1,1 @@
+List_Examples = Hoare + List
diff -r 5fdd4da11d49 -r 7bdc4699ef4d src/HOL/Hoare/ROOT.ML
--- a/src/HOL/Hoare/ROOT.ML	Tue Nov 21 17:59:45 1995 +0100
+++ b/src/HOL/Hoare/ROOT.ML	Wed Nov 22 18:48:56 1995 +0100
@@ -7,3 +7,4 @@
 HOL_build_completed;	(*Make examples fail if HOL did*)
 
 use_thy "Examples";
+use_thy "List_Examples";