tuned proof; tuned headers
authorhaftmann
Mon Sep 21 14:23:04 2009 +0200 (2009-09-21)
changeset 32689860e1a2317bd
parent 32688 58b561b415a2
child 32690 5fb07ec99828
tuned proof; tuned headers
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/UNITY_Main.thy
     1.1 --- a/src/HOL/UNITY/Follows.thy	Mon Sep 21 12:24:21 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Follows.thy	Mon Sep 21 14:23:04 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/UNITY/Follows
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1998  University of Cambridge
     1.8  *)
     1.9 @@ -160,7 +159,7 @@
    1.10  lemma Follows_Un: 
    1.11      "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
    1.12       ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
    1.13 -apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
    1.14 +apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
    1.15  apply (rule LeadsTo_Trans)
    1.16  apply (blast intro: Follows_Un_lemma)
    1.17  (*Weakening is used to exchange Un's arguments*)
     2.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 12:24:21 2009 +0200
     2.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Sep 21 14:23:04 2009 +0200
     2.3 @@ -1,13 +1,14 @@
     2.4  (*  Title:      HOL/UNITY/UNITY_Main.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Copyright   2003  University of Cambridge
     2.8  *)
     2.9  
    2.10  header{*Comprehensive UNITY Theory*}
    2.11  
    2.12 -theory UNITY_Main imports Detects PPROD Follows ProgressSets
    2.13 -uses "UNITY_tactics.ML" begin
    2.14 +theory UNITY_Main
    2.15 +imports Detects PPROD Follows ProgressSets
    2.16 +uses "UNITY_tactics.ML"
    2.17 +begin
    2.18  
    2.19  method_setup safety = {*
    2.20      Scan.succeed (fn ctxt =>