isabelle: src/HOL/Trancl.thy@bb7622789bf2 (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
3499 ce1664057431 Reduced priority of postfix ^* etc operators such that they are the same as nipkow parents: 1916 diff changeset	19	rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [1000] 999)
5608 a82a038a3e7a id <-> Id nipkow parents: 3499 diff changeset	20	"r^* == lfp(%s. Id Un (r O s))"
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	21
3499 ce1664057431 Reduced priority of postfix ^* etc operators such that they are the same as nipkow parents: 1916 diff changeset	22	trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [1000] 999)
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
6906 46652582f831 _reflcl; wenzelm parents: 5608 diff changeset	26	"_reflcl" :: "('a'a)set => ('a'a)set" ("(_^=)" [1000] 999)
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
5608 a82a038a3e7a id <-> Id nipkow parents: 3499 diff changeset	29	"r^=" == "r Un Id"
1558 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	wenzelm
	Sat, 03 Jun 2000 23:57:40 +0200
changeset 9030	bb7622789bf2
parent 6906	46652582f831
permissions	-rw-r--r--