isabelle: src/HOL/Library/FinFun_Syntax.thy@745d31e63c21 (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
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 61384 diff changeset	16	finfun_comp (infixr "\<circ>$" 55) and
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 61384 diff changeset	17	finfun_comp2 (infixr "$\<circ>" 55) and
48041 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
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 61384 diff changeset	20	notation (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 61384 diff changeset	21	finfun_comp (infixr "o$" 55) and
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 61384 diff changeset	22	finfun_comp2 (infixr "$o" 55)
48041 d60f6b41bf2d remove pretty syntax for FinFuns at the end and provide separate syntax theory Andreas Lochbihler parents: diff changeset	23
62390 842917225d56 more canonical names nipkow parents: 61955 diff changeset	24	end

author	wenzelm
	Thu, 07 Apr 2016 22:09:23 +0200
changeset 62912	745d31e63c21
parent 62390	842917225d56
permissions	-rw-r--r--