nominal2: Attic/Quot/Quotient_Syntax.thy@2fc55508a6d0 (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	Christian Urban <urbanc@in.tum.de>
	Fri, 14 May 2010 17:40:43 +0100
changeset 2136	2fc55508a6d0
parent 1260	9df6144e281b
permissions	-rw-r--r--