nominal2: Attic/Quot/Quotient_Syntax.thy@f89773ab0685 (annotated)

1148 389d81959922 Names of files. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1130 diff changeset	1	(* Title: Quotient_Syntax.thy
389d81959922 Names of files. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1130 diff changeset	2	Author: Cezary Kaliszyk and Christian Urban
389d81959922 Names of files. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1130 diff changeset	3	*)
389d81959922 Names of files. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1130 diff changeset	4
1130 fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	5	header {* Pretty syntax for Quotient operations *}
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	6
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	(<)
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	theory Quotient_Syntax
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	imports Quotient
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10	begin
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	11
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	12	notation
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	rel_conj (infixr "OOO" 75) and
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	fun_map (infixr "--->" 55) and
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15	fun_rel (infixr "===>" 55)
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	16
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	17	end
fb5f5735a426 Added the missing syntax file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	18	(>)

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 17 May 2010 16:29:33 +0200
changeset 2145	f89773ab0685
parent 1260	9df6144e281b
permissions	-rw-r--r--