Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/FinFun_Syntax.thy
author wenzelm
Fri, 06 Mar 2015 15:58:56 +0100
changeset 59621 291934bac95e
parent 58881 b9556a055632
child 60500 903bb1495239
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
 







58881






b9556a055632
modernized header;



wenzelm


parents: 
51542

diff
changeset




     3


section {* Pretty syntax for almost everywhere constant functions *}








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 ("(_ =>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














isabelle