export vars_of;
authorwenzelm
Mon Mar 13 13:19:14 2000 +0100 (2000-03-13)
changeset 8431e5f8ee756a8a
parent 8430 dbd897e0d804
child 8432 daf6b3961ed4
export vars_of;
src/HOL/Tools/induct_method.ML
     1.1 --- a/src/HOL/Tools/induct_method.ML	Mon Mar 13 13:18:59 2000 +0100
     1.2 +++ b/src/HOL/Tools/induct_method.ML	Mon Mar 13 13:19:14 2000 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4      {type_cases: (string * thm) list, set_cases: (string * thm) list,
     1.5        type_induct: (string * thm) list, set_induct: (string * thm) list}
     1.6    val print_local_rules: Proof.context -> unit
     1.7 +  val vars_of: term -> term list
     1.8    val cases_type_global: string -> theory attribute
     1.9    val cases_set_global: string -> theory attribute
    1.10    val cases_type_local: string -> Proof.context attribute