src/HOL/indrule.ML
changeset 1653 1a2ffa2fbf7d
parent 1465 5d7a7e439cec
child 1728 01beef6262aa
equal deleted inserted replaced
1652:9b78ce58d6b1 1653:1a2ffa2fbf7d
    88                             Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp 
    88                             Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp 
    89                                                     (big_rec_tm,pred)))))
    89                                                     (big_rec_tm,pred)))))
    90       (fn prems =>
    90       (fn prems =>
    91        [rtac (impI RS allI) 1,
    91        [rtac (impI RS allI) 1,
    92         DETERM (etac Intr_elim.raw_induct 1),
    92         DETERM (etac Intr_elim.raw_induct 1),
    93         asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1,
    93         asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1,
    94         REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
    94         REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
    95                            ORELSE' hyp_subst_tac)),
    95                            ORELSE' hyp_subst_tac)),
    96         ind_tac (rev prems) (length prems)])
    96         ind_tac (rev prems) (length prems)])
    97     handle e => print_sign_exn sign e;
    97     handle e => print_sign_exn sign e;
    98 
    98