src/Provers/induct_method.ML
Wed, 31 Oct 2001 01:28:39 +0100 wenzelm induct: internalize ``missing'' consumes-facts from goal state
Tue, 30 Oct 2001 17:30:21 +0100 wenzelm induct: cases are extracted from rulified rule;
Tue, 16 Oct 2001 17:56:12 +0200 wenzelm dest_env: norm_term on rhs;
Tue, 16 Oct 2001 00:32:01 +0200 wenzelm simplified resolveq_cases_tac for cases, separate version for induct;
Mon, 15 Oct 2001 20:35:10 +0200 wenzelm Tactic.rewrite_cterm;
Sun, 14 Oct 2001 22:15:07 +0200 wenzelm moved rulify to ObjectLogic;
Sun, 14 Oct 2001 20:05:42 +0200 wenzelm use ObjectLogic stuff;
Fri, 12 Oct 2001 12:13:31 +0200 wenzelm removed vars_of, concls_of;
Thu, 04 Oct 2001 15:20:40 +0200 wenzelm proof by cases and induction on types and sets (used to be specific for HOL);
less more (0) tip