src/Doc/Classes/Setup.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 51143 0a2371e7ced3
child 52143 36ffe23b25f8
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28565
haftmann
parents:
diff changeset
     1
theory Setup
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
     2
imports Main
28565
haftmann
parents:
diff changeset
     3
begin
haftmann
parents:
diff changeset
     4
48950
9965099f51ad more standard document preparation within session context;
wenzelm
parents: 48891
diff changeset
     5
ML_file "../antiquote_setup.ML"
9965099f51ad more standard document preparation within session context;
wenzelm
parents: 48891
diff changeset
     6
ML_file "../more_antiquote.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset
     7
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42224
diff changeset
     8
setup {*
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42224
diff changeset
     9
  Antiquote_Setup.setup #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42224
diff changeset
    10
  More_Antiquote.setup #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42224
diff changeset
    11
  Code_Target.set_default_code_width 74
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42224
diff changeset
    12
*}
28565
haftmann
parents:
diff changeset
    13
haftmann
parents:
diff changeset
    14
syntax
haftmann
parents:
diff changeset
    15
  "_alpha" :: "type"  ("\<alpha>")
haftmann
parents:
diff changeset
    16
  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
haftmann
parents:
diff changeset
    17
  "_beta" :: "type"  ("\<beta>")
haftmann
parents:
diff changeset
    18
  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
haftmann
parents:
diff changeset
    19
haftmann
parents:
diff changeset
    20
parse_ast_translation {*
haftmann
parents:
diff changeset
    21
  let
42224
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    22
    fun alpha_ast_tr [] = Ast.Variable "'a"
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    23
      | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
28565
haftmann
parents:
diff changeset
    24
    fun alpha_ofsort_ast_tr [ast] =
42224
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    25
          Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    26
      | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    27
    fun beta_ast_tr [] = Ast.Variable "'b"
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    28
      | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
28565
haftmann
parents:
diff changeset
    29
    fun beta_ofsort_ast_tr [ast] =
42224
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    30
          Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
578a51fae383 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents: 41413
diff changeset
    31
      | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    32
  in
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    33
   [(@{syntax_const "_alpha"}, alpha_ast_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    34
    (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    35
    (@{syntax_const "_beta"}, beta_ast_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    36
    (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
1a0c129bb2e0 modernized translations;
wenzelm
parents: 34071
diff changeset
    37
  end
28565
haftmann
parents:
diff changeset
    38
*}
haftmann
parents:
diff changeset
    39
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48985
diff changeset
    40
end