isabelle: src/HOL/Library/Quotient_Syntax.thy@396676efbd6d (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
80914 d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 60500 diff changeset	12	rel_conj (infixr \<open>OOO\<close> 75) and
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 60500 diff changeset	13	map_fun (infixr \<open>--->\<close> 55) and
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 60500 diff changeset	14	rel_fun (infixr \<open>===>\<close> 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	desharna
	Thu, 27 Mar 2025 13:44:42 +0100
changeset 82362	396676efbd6d
parent 80914	d97fdabd9e2b
permissions	-rw-r--r--