doc-src/Classes/Thy/Setup.thy
author boehmes
Tue, 07 Dec 2010 15:44:38 +0100
changeset 41064 0c447a17770a
parent 38321 7edf0ab9d5cb
child 41413 64cd30d6b0b8
permissions -rw-r--r--
updated SMT certificates
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28565
haftmann
parents:
diff changeset
     1
theory Setup
haftmann
parents:
diff changeset
     2
imports Main Code_Integer
haftmann
parents:
diff changeset
     3
uses
38321
7edf0ab9d5cb explicit ML extension
haftmann
parents: 35113
diff changeset
     4
  "../../antiquote_setup.ML"
7edf0ab9d5cb explicit ML extension
haftmann
parents: 35113
diff changeset
     5
  "../../more_antiquote.ML"
28565
haftmann
parents:
diff changeset
     6
begin
haftmann
parents:
diff changeset
     7
34071
93bfbb557e2e default_code_width is now proper theory data
haftmann
parents: 30227
diff changeset
     8
setup {* Code_Target.set_default_code_width 74 *}
28565
haftmann
parents:
diff changeset
     9
haftmann
parents:
diff changeset
    10
syntax
haftmann
parents:
diff changeset
    11
  "_alpha" :: "type"  ("\<alpha>")
haftmann
parents:
diff changeset
    12
  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
haftmann
parents:
diff changeset
    13
  "_beta" :: "type"  ("\<beta>")
haftmann
parents:
diff changeset
    14
  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
haftmann
parents:
diff changeset
    15
haftmann
parents:
diff changeset
    16
parse_ast_translation {*
haftmann
parents:
diff changeset
    17
  let
haftmann
parents:
diff changeset
    18
    fun alpha_ast_tr [] = Syntax.Variable "'a"
haftmann
parents:
diff changeset
    19
      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
haftmann
parents:
diff changeset
    20
    fun alpha_ofsort_ast_tr [ast] =
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    21
      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
28565
haftmann
parents:
diff changeset
    22
      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
haftmann
parents:
diff changeset
    23
    fun beta_ast_tr [] = Syntax.Variable "'b"
haftmann
parents:
diff changeset
    24
      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
haftmann
parents:
diff changeset
    25
    fun beta_ofsort_ast_tr [ast] =
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    26
      Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
28565
haftmann
parents:
diff changeset
    27
      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    28
  in
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    29
   [(@{syntax_const "_alpha"}, alpha_ast_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    30
    (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    31
    (@{syntax_const "_beta"}, beta_ast_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    32
    (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    33
  end
28565
haftmann
parents:
diff changeset
    34
*}
haftmann
parents:
diff changeset
    35
haftmann
parents:
diff changeset
    36
end