# HG changeset patch
# User oheimb
# Date 982249011 -3600
# Node ID 09622301ca078d3d7ad05d4195b1deacf8ad55e6
# Parent  5dc3b5abdbca4381d6e50433c7b23e9cab693d9c
added trial proof

diff -r 5dc3b5abdbca -r 09622301ca07 src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Thu Feb 15 14:30:13 2001 +0100
+++ b/src/HOL/IMPP/Hoare.ML	Thu Feb 15 15:56:51 2001 +0100
@@ -405,3 +405,23 @@
 by (etac spec 1);
 qed "weak_Local";
 
+(*
+Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}";
+by (induct_tac "c" 1);
+auto();
+br conseq1 1;
+br hoare_derivs.Skip 1;
+force 1;
+br conseq1 1;
+br hoare_derivs.Ass 1;
+force 1;
+by (defer_tac 1);
+###
+br hoare_derivs.Comp 1;
+bd spec 2;
+bd spec 2;
+ba 2;
+be conseq1 2;
+by (Clarsimp_tac 2);
+force 1;
+*)