isabelle: src/HOL/Library/Quotient_Syntax.thy@438d583ab378 (annotated)

35787 afdf1c4958b2 expose formal text; wenzelm parents: 35222 diff changeset	1	(* Title: HOL/Library/Quotient_Syntax.thy
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	Author: Cezary Kaliszyk and Christian Urban
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	*)
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	4
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	5	section \<open>Pretty syntax for Quotient operations\<close>
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	theory Quotient_Syntax
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	imports Main
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	begin
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11	notation
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	rel_conj (infixr "OOO" 75) and
40602 91e583511113 map_fun combinator in theory Fun haftmann parents: 35787 diff changeset	13	map_fun (infixr "--->" 55) and
55945 e96383acecf9 renamed 'fun_rel' to 'rel_fun' blanchet parents: 40602 diff changeset	14	rel_fun (infixr "===>" 55)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16	end

author	wenzelm
	Sun, 12 May 2024 14:41:13 +0200
changeset 80178	438d583ab378
parent 60500	903bb1495239
child 80914	d97fdabd9e2b
permissions	-rw-r--r--