isabelle: src/HOL/UNITY/Follows.thy@e36798726ca4 (annotated)

6706 d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	1	(* Title: HOL/UNITY/Follows
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	2	ID: $Id$
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	5
8128 3a5864b465e2 still working; a bit of polishing paulson parents: 8122 diff changeset	6	The "Follows" relation of Charpentier and Sivilotte
6706 d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	7	*)
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	8
10265 4e004b548049 use Multiset from HOL/Library; wenzelm parents: 9019 diff changeset	9	Follows = SubstAx + ListOrder + Multiset +
6706 d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	10
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	11	constdefs
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	12
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	13	Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
6809 5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	14	(infixl "Fols" 65)
5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	15	"f Fols g == Increasing g Int Increasing f Int
5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	16	Always {s. f s <= g s} Int
5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	17	(INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
6706 d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	18
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	19
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	20	end

author	berghofe
	Mon, 21 Oct 2002 17:07:58 +0200
changeset 13660	e36798726ca4
parent 10265	4e004b548049
child 13796	19f50fa807ae
permissions	-rw-r--r--