src/Pure/Isar/isar_thy.ML
changeset 8227 d67db92897df
parent 8213 a541e261c660
child 8236 df3f983f5858
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Feb 10 11:08:42 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Feb 10 13:34:38 2000 +0100
     1.3 @@ -41,6 +41,8 @@
     1.4      -> theory -> theory
     1.5    val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list -> theory -> theory
     1.6    val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list -> theory -> theory
     1.7 +  val add_judgment: (bstring * string * mixfix) * Comment.text -> theory -> theory
     1.8 +  val add_judgment_i: (bstring * typ * mixfix) * Comment.text -> theory -> theory
     1.9    val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
    1.10    val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
    1.11      -> theory -> theory
    1.12 @@ -207,7 +209,8 @@
    1.13  fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore;
    1.14  val add_trrules = Theory.add_trrules o map Comment.ignore;
    1.15  val add_trrules_i = Theory.add_trrules_i o map Comment.ignore;
    1.16 -
    1.17 +val add_judgment = AutoBind.add_judgment o Comment.ignore;
    1.18 +val add_judgment_i = AutoBind.add_judgment_i o Comment.ignore;
    1.19  
    1.20  
    1.21  (* axioms and defs *)