nominal2: Quot/Quotient_Syntax.thy@59dc48db4a84 (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>
	Tue, 23 Feb 2010 18:28:48 +0100
changeset 1231	59dc48db4a84
parent 1148	389d81959922
permissions	-rw-r--r--