doc-src/IsarAdvanced/Classes/Thy/Setup.thy
changeset 28565 519b17118926
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Setup.thy	Fri Oct 10 15:52:45 2008 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +theory Setup
     1.5 +imports Main Code_Integer
     1.6 +uses
     1.7 +  "../../../antiquote_setup"
     1.8 +  "../../../more_antiquote"
     1.9 +begin
    1.10 +
    1.11 +ML {* Code_Target.code_width := 74 *}
    1.12 +
    1.13 +syntax
    1.14 +  "_alpha" :: "type"  ("\<alpha>")
    1.15 +  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
    1.16 +  "_beta" :: "type"  ("\<beta>")
    1.17 +  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
    1.18 +
    1.19 +parse_ast_translation {*
    1.20 +  let
    1.21 +    fun alpha_ast_tr [] = Syntax.Variable "'a"
    1.22 +      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    1.23 +    fun alpha_ofsort_ast_tr [ast] =
    1.24 +      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
    1.25 +      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    1.26 +    fun beta_ast_tr [] = Syntax.Variable "'b"
    1.27 +      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    1.28 +    fun beta_ofsort_ast_tr [ast] =
    1.29 +      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
    1.30 +      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    1.31 +  in [
    1.32 +    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
    1.33 +    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
    1.34 +  ] end
    1.35 +*}
    1.36 +
    1.37 +end
    1.38 \ No newline at end of file