src/Doc/Classes/Setup.thy

some new results in group theory

theory Setup
imports Main
begin

ML_file \<open>../antiquote_setup.ML\<close>
ML_file \<open>../more_antiquote.ML\<close>

declare [[default_code_width = 74]]

syntax
  "_alpha" :: "type"  ("\<alpha>")
  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()::_" [0] 1000)
  "_beta" :: "type"  ("\<beta>")
  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()::_" [0] 1000)

parse_ast_translation \<open>
  let
    fun alpha_ast_tr [] = Ast.Variable "'a"
      | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
    fun alpha_ofsort_ast_tr [ast] =
          Ast.Appl [Ast.Constant \<^syntax_const>\<open>_ofsort\<close>, Ast.Variable "'a", ast]
      | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
    fun beta_ast_tr [] = Ast.Variable "'b"
      | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
    fun beta_ofsort_ast_tr [ast] =
          Ast.Appl [Ast.Constant \<^syntax_const>\<open>_ofsort\<close>, Ast.Variable "'b", ast]
      | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
  in
   [(\<^syntax_const>\<open>_alpha\<close>, K alpha_ast_tr),
    (\<^syntax_const>\<open>_alpha_ofsort\<close>, K alpha_ofsort_ast_tr),
    (\<^syntax_const>\<open>_beta\<close>, K beta_ast_tr),
    (\<^syntax_const>\<open>_beta_ofsort\<close>, K beta_ofsort_ast_tr)]
  end
\<close>

end