src/HOL/UNITY/Follows.thy
changeset 6809 5b8912f7bb69
parent 6706 d8067e272d4f
child 8074 36a6c38e0eca
     1.1 --- a/src/HOL/UNITY/Follows.thy	Thu Jun 10 10:37:29 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Follows.thy	Thu Jun 10 10:38:11 1999 +0200
     1.3 @@ -11,10 +11,10 @@
     1.4  constdefs
     1.5  
     1.6    Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
     1.7 -                 (infixl 65)
     1.8 -   "f Follows g == Increasing g Int Increasing f Int
     1.9 -                   Always {s. f s <= g s} Int
    1.10 -                   (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
    1.11 +                 (infixl "Fols" 65)
    1.12 +   "f Fols g == Increasing g Int Increasing f Int
    1.13 +                Always {s. f s <= g s} Int
    1.14 +                (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
    1.15  
    1.16  
    1.17  end