src/Doc/Classes/Setup.thy
changeset 71546 4dd5dadfc87d
parent 69605 a96320074298
equal deleted inserted replaced
71545:b0b16088ccf2 71546:4dd5dadfc87d
     7 
     7 
     8 declare [[default_code_width = 74]]
     8 declare [[default_code_width = 74]]
     9 
     9 
    10 syntax
    10 syntax
    11   "_alpha" :: "type"  ("\<alpha>")
    11   "_alpha" :: "type"  ("\<alpha>")
    12   "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()::_" [0] 1000)
    12   "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>' ::_" [0] 1000)
    13   "_beta" :: "type"  ("\<beta>")
    13   "_beta" :: "type"  ("\<beta>")
    14   "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()::_" [0] 1000)
    14   "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>' ::_" [0] 1000)
    15 
    15 
    16 parse_ast_translation \<open>
    16 parse_ast_translation \<open>
    17   let
    17   let
    18     fun alpha_ast_tr [] = Ast.Variable "'a"
    18     fun alpha_ast_tr [] = Ast.Variable "'a"
    19       | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
    19       | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);