author | paulson |
Fri, 21 Jul 2000 18:01:36 +0200 | |
changeset 9403 | aad13b59b8d9 |
parent 9019 | 9c1118619d6c |
child 10265 | 4e004b548049 |
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 add_path "../Induct"; *) Follows = SubstAx + ListOrder + MultisetOrder + 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