isabelle: src/HOL/Library/FinFun_Syntax.thy@e96383acecf9 (annotated)

48041 d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	1	(* Author: Andreas Lochbihler, KIT *)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	2
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	3	header {* Pretty syntax for almost everywhere constant functions *}
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	4
51542 738598beeb26 tuned imports; wenzelm parents: 48041 diff changeset	5	theory FinFun_Syntax
738598beeb26 tuned imports; wenzelm parents: 48041 diff changeset	6	imports FinFun
738598beeb26 tuned imports; wenzelm parents: 48041 diff changeset	7	begin
48041 d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	8
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	9	type_notation
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	10	finfun ("(_ =>f /_)" [22, 21] 21)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	11
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	12	type_notation (xsymbols)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	13	finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	14
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	15	notation
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	16	finfun_const ("K$/ _" [0] 1) and
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	17	finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	18	finfun_apply (infixl "$" 999) and
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	19	finfun_comp (infixr "o$" 55) and
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	20	finfun_comp2 (infixr "$o" 55) and
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	21	finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	22
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	23	notation (xsymbols)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	24	finfun_comp (infixr "\<circ>$" 55) and
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	25	finfun_comp2 (infixr "$\<circ>" 55)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	26
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	27	end

author	blanchet
	Thu, 06 Mar 2014 15:40:33 +0100
changeset 55945	e96383acecf9
parent 51542	738598beeb26
child 58881	b9556a055632
permissions	-rw-r--r--