--- a/src/HOL/UNITY/Follows.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/UNITY/Follows.thy Mon Mar 01 13:40:23 2010 +0100
@@ -7,10 +7,7 @@
theory Follows imports SubstAx ListOrder Multiset begin
-constdefs
-
- Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
- (infixl "Fols" 65)
+definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where
"f Fols g == Increasing g \<inter> Increasing f Int
Always {s. f s \<le> g s} Int
(\<Inter>k. {s. k \<le> g s} LeadsTo {s. k \<le> f s})"