equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 section\<open>The Follows Relation of Charpentier and Sivilotte\<close> |
6 section\<open>The Follows Relation of Charpentier and Sivilotte\<close> |
7 |
7 |
8 theory Follows |
8 theory Follows |
9 imports SubstAx ListOrder "~~/src/HOL/Library/Multiset" |
9 imports SubstAx ListOrder "HOL-Library.Multiset" |
10 begin |
10 begin |
11 |
11 |
12 definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where |
12 definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where |
13 "f Fols g == Increasing g \<inter> Increasing f Int |
13 "f Fols g == Increasing g \<inter> Increasing f Int |
14 Always {s. f s \<le> g s} Int |
14 Always {s. f s \<le> g s} Int |