src/Pure/Isar/isar_thy.ML
changeset 12271 37b9c807b461
parent 12244 179f142ffb03
child 12318 72348ff7d4a0
equal deleted inserted replaced
12270:71534648d5d4 12271:37b9c807b461
   186   val typed_print_translation: string * Comment.text -> theory -> theory
   186   val typed_print_translation: string * Comment.text -> theory -> theory
   187   val print_ast_translation: string * Comment.text -> theory -> theory
   187   val print_ast_translation: string * Comment.text -> theory -> theory
   188   val token_translation: string * Comment.text -> theory -> theory
   188   val token_translation: string * Comment.text -> theory -> theory
   189   val method_setup: (bstring * string * string) * Comment.text -> theory -> theory
   189   val method_setup: (bstring * string * string) * Comment.text -> theory -> theory
   190   val add_oracle: (bstring * string) * Comment.text -> theory -> theory
   190   val add_oracle: (bstring * string) * Comment.text -> theory -> theory
   191   val add_locale: bstring * xstring list * (Args.src Locale.element * Comment.text) list
   191   val add_locale: bstring * Locale.expr * (Args.src Locale.element * Comment.text) list
   192     -> theory -> theory
   192     -> theory -> theory
   193   val begin_theory: string -> string list -> (string * bool) list -> theory
   193   val begin_theory: string -> string list -> (string * bool) list -> theory
   194   val end_theory: theory -> theory
   194   val end_theory: theory -> theory
   195   val kill_theory: string -> unit
   195   val kill_theory: string -> unit
   196   val theory: string * string list * (string * bool) list
   196   val theory: string * string list * (string * bool) list