author | paulson |
Fri, 14 Jan 2000 12:17:53 +0100 | |
changeset 8128 | 3a5864b465e2 |
parent 8122 | b43ad07660b9 |
child 8948 | b797cfa3548d |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/Follows ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge The "Follows" relation of Charpentier and Sivilotte *) Follows = SubstAx + constdefs Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) "f Fols g == Increasing g Int Increasing f Int Always {s. f s <= g s} Int (INT k. {s. k <= g s} LeadsTo {s. k <= f s})" end