isabelle: src/HOL/Library/Quotient_Syntax.thy@91f9e4148460 (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
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	header {* Pretty syntax for Quotient operations *}
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	haftmann
	Sat, 28 Jun 2014 21:09:17 +0200
changeset 57427	91f9e4148460
parent 55945	e96383acecf9
child 58881	b9556a055632
permissions	-rw-r--r--