src/Pure/theory.ML
changeset 17038 6dbd7c63a5a6
parent 16991 39f5760f72d7
child 17496 26535df536ae
     1.1 --- a/src/Pure/theory.ML	Tue Aug 09 10:03:30 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Aug 09 10:23:14 2005 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4    val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
     1.5    val requires: theory -> string -> string -> unit
     1.6    val assert_super: theory -> theory -> theory
     1.7 +  val dest_def: Pretty.pp -> term -> (string * typ) * term
     1.8    val add_axioms: (bstring * string) list -> theory -> theory
     1.9    val add_axioms_i: (bstring * term) list -> theory -> theory
    1.10    val add_defs: bool -> (bstring * string) list -> theory -> theory