isabelle: src/HOL/UNITY/Follows.thy@50be659d4222 (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
9019 9c1118619d6c new parent MultisetOrder and new results about multiset unions paulson parents: 8948 diff changeset	7
9c1118619d6c new parent MultisetOrder and new results about multiset unions paulson parents: 8948 diff changeset	8	add_path "../Induct";
6706 d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	9	*)
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	10
9019 9c1118619d6c new parent MultisetOrder and new results about multiset unions paulson parents: 8948 diff changeset	11	Follows = SubstAx + ListOrder + MultisetOrder +
6706 d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	12
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	13	constdefs
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	14
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	15	Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
6809 5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	16	(infixl "Fols" 65)
5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	17	"f Fols g == Increasing g Int Increasing f Int
5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	18	Always {s. f s <= g s} Int
5b8912f7bb69 shortened Follows to Fols paulson parents: 6706 diff changeset	19	(INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
6706 d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	20
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	21
d8067e272d4f Theory of the "Follows" relation paulson parents: diff changeset	22	end

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9019	9c1118619d6c
child 10265	4e004b548049
permissions	-rw-r--r--