src/HOL/Tools/datatype_package.ML
changeset 9747 043098ba5098
parent 9739 8470c4662685
child 10121 fb9be005cc44
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Aug 30 16:24:29 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Aug 30 16:29:21 2000 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  signature BASIC_DATATYPE_PACKAGE =
     1.5  sig
     1.6    val induct_tac : string -> int -> tactic
     1.7 +  val induct_thm_tac : thm -> string -> int -> tactic
     1.8    val case_tac : string -> int -> tactic
     1.9    val distinct_simproc : simproc
    1.10  end;
    1.11 @@ -199,6 +200,9 @@
    1.12  
    1.13  fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
    1.14  
    1.15 +fun induct_thm_tac th s =
    1.16 +  gen_induct_tac ([map Some (Syntax.read_idents s)], Some th);
    1.17 +
    1.18  end;
    1.19  
    1.20