summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Fri, 21 Nov 2008 13:17:43 +0100 | |

changeset 28869 | 191cbfac6c9a |

parent 28868 | 4fe0e90080ce |

child 28870 | 381a3b3139ae |

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.

--- 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