# HG changeset patch
# User paulson
# Date 937817130 -7200
# Node ID b6599e2920112081777ae5dafc0c2d512f436d1b
# Parent  1a7a38d8f5bd682ebf1afff8e49b86d369733b24
new theorem mono_Follows_apply

diff -r 1a7a38d8f5bd -r b6599e292011 src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Mon Sep 20 10:42:09 1999 +0200
+++ b/src/HOL/UNITY/Follows.ML	Mon Sep 20 10:45:30 1999 +0200
@@ -30,6 +30,11 @@
 			 impOfSubs mono_LeadsTo_o RS INT_D]) 1);
 qed "mono_Follows_o";
 
+Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";
+by (dtac mono_Follows_o 1);
+by (force_tac (claset(), simpset() addsimps [o_def]) 1);
+qed "mono_Follows_apply";
+
 Goalw [Follows_def]
      "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h";
 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);