isabelle: src/HOL/Trancl.thy@aa5aeb6467c6 (annotated)

1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1301 diff changeset	1	(* Title: HOL/Trancl.thy
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1301 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
1128 64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ. nipkow parents: 972 diff changeset	6	Relfexive and Transitive closure of a relation
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7
1642 21db0cf9a1a4 Using new "Times" infix paulson parents: 1558 diff changeset	8	rtrancl is reflexive/transitive closure;
21db0cf9a1a4 Using new "Times" infix paulson parents: 1558 diff changeset	9	trancl is transitive closure
21db0cf9a1a4 Using new "Times" infix paulson parents: 1558 diff changeset	10	reflcl is reflexive closure
1916 43521f79f016 Changed precedences to remove ambiguities in r^+ notation paulson parents: 1642 diff changeset	11
43521f79f016 Changed precedences to remove ambiguities in r^+ notation paulson parents: 1642 diff changeset	12	These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
43521f79f016 Changed precedences to remove ambiguities in r^+ notation paulson parents: 1642 diff changeset	13	atomic.
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	15
1128 64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ. nipkow parents: 972 diff changeset	16	Trancl = Lfp + Relation +
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	17
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	18	constdefs
1916 43521f79f016 Changed precedences to remove ambiguities in r^+ notation paulson parents: 1642 diff changeset	19	rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [1000] 1000)
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	20	"r^* == lfp(%s. id Un (r O s))"
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	21
1916 43521f79f016 Changed precedences to remove ambiguities in r^+ notation paulson parents: 1642 diff changeset	22	trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [1000] 1000)
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	23	"r^+ == r O rtrancl(r)"
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	24
1301 42782316d510 Added various thms and tactics. nipkow parents: 1287 diff changeset	25	syntax
1916 43521f79f016 Changed precedences to remove ambiguities in r^+ notation paulson parents: 1642 diff changeset	26	reflcl :: "('a'a)set => ('a'a)set" ("(_^=)" [1000] 1000)
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	27
1301 42782316d510 Added various thms and tactics. nipkow parents: 1287 diff changeset	28	translations
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	29	"r^=" == "r Un id"
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	30
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	31	end

author	paulson
	Fri, 18 Apr 1997 11:47:11 +0200
changeset 2981	aa5aeb6467c6
parent 1916	43521f79f016
child 3499	ce1664057431
permissions	-rw-r--r--