# HG changeset patch
# User paulson
# Date 1227269863 -3600
# Node ID 191cbfac6c9aadd3d6c0979ad85ee2b7076bb75b
# Parent  4fe0e90080ce6de8ab4b47c346d32b1dd36b9979
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.

diff -r 4fe0e90080ce -r 191cbfac6c9a src/HOL/UNITY/Comp/Progress.thy
--- a/src/HOL/UNITY/Comp/Progress.thy	Fri Nov 21 07:34:36 2008 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy	Fri Nov 21 13:17:43 2008 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Transformers
+(*  Title:      HOL/UNITY/Progress
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
@@ -93,12 +93,9 @@
 apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
  apply simp
 apply (rule_tac T = "atLeast 0" in leadsTo_Join)
-oops
-(* FIXME rotten proof
-  apply (simp add: awp_iff_constrains FF_def, safety)
- apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety)
-apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) 
+  apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) 
+ apply (simp add: awp_iff_constrains FF_def, safety)
+apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety)
 done
-*)
 
 end