# HG changeset patch
# User haftmann
# Date 1253535784 -7200
# Node ID 860e1a2317bd09ae55e3f428d1bd3ad7a3a9cbee
# Parent  58b561b415a2b9bfb000b59187685eb89c7247ad
tuned proof; tuned headers

diff -r 58b561b415a2 -r 860e1a2317bd src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Mon Sep 21 12:24:21 2009 +0200
+++ b/src/HOL/UNITY/Follows.thy	Mon Sep 21 14:23:04 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/Follows
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
@@ -160,7 +159,7 @@
 lemma Follows_Un: 
     "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
      ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
-apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
+apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
 apply (rule LeadsTo_Trans)
 apply (blast intro: Follows_Un_lemma)
 (*Weakening is used to exchange Un's arguments*)
diff -r 58b561b415a2 -r 860e1a2317bd src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 12:24:21 2009 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 14:23:04 2009 +0200
@@ -1,13 +1,14 @@
 (*  Title:      HOL/UNITY/UNITY_Main.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
 *)
 
 header{*Comprehensive UNITY Theory*}
 
-theory UNITY_Main imports Detects PPROD Follows ProgressSets
-uses "UNITY_tactics.ML" begin
+theory UNITY_Main
+imports Detects PPROD Follows ProgressSets
+uses "UNITY_tactics.ML"
+begin
 
 method_setup safety = {*
     Scan.succeed (fn ctxt =>