isabelle: src/HOL/Library/FinFun_Syntax.thy@d50b993b4fb9 (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
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	3	section \<open>Pretty syntax for almost everywhere constant functions\<close>
48041 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 ("(_ \<Rightarrow>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	notation
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	13	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	14	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	15	finfun_apply (infixl "$" 999) and
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	16	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	17	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	18	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	19
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	20	notation (xsymbols)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	21	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	22	finfun_comp2 (infixr "$\<circ>" 55)
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	23
d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	24	end

author	paulson <lp15@cam.ac.uk>
	Tue, 01 Dec 2015 14:09:10 +0000
changeset 61762	d50b993b4fb9
parent 61384	9f5145281888
child 61955	e96292f32c3c
permissions	-rw-r--r--