isabelle: src/HOL/UNITY/Follows.thy@b797cfa3548d (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
8948 b797cfa3548d restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML paulson parents: 8128 diff changeset	9	Follows = SubstAx + ListOrder +
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	paulson
	Wed, 24 May 2000 18:40:01 +0200
changeset 8948	b797cfa3548d
parent 8128	3a5864b465e2
child 9019	9c1118619d6c
permissions	-rw-r--r--