doc-src/IsarAdvanced/Classes/Thy/Setup.thy
author haftmann
Fri Oct 10 15:52:45 2008 +0200 (2008-10-10)
changeset 28565 519b17118926
permissions -rw-r--r--
tuned
     1 theory Setup
     2 imports Main Code_Integer
     3 uses
     4   "../../../antiquote_setup"
     5   "../../../more_antiquote"
     6 begin
     7 
     8 ML {* Code_Target.code_width := 74 *}
     9 
    10 syntax
    11   "_alpha" :: "type"  ("\<alpha>")
    12   "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
    13   "_beta" :: "type"  ("\<beta>")
    14   "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
    15 
    16 parse_ast_translation {*
    17   let
    18     fun alpha_ast_tr [] = Syntax.Variable "'a"
    19       | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    20     fun alpha_ofsort_ast_tr [ast] =
    21       Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
    22       | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    23     fun beta_ast_tr [] = Syntax.Variable "'b"
    24       | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    25     fun beta_ofsort_ast_tr [ast] =
    26       Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
    27       | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    28   in [
    29     ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
    30     ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
    31   ] end
    32 *}
    33 
    34 end