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