2001-11-12 ago wenzelm mutual rules declared as ``consumes 0'';
2001-11-12 ago wenzelm induct_atomize: include atomize_conj (for mutual induction);
2001-11-12 ago wenzelm Isar: 'induct' proper support for mutual induction involving
2001-11-12 ago wenzelm proper handling of mutual rules (esp. for sets);
2001-11-12 ago wenzelm lemmas induct_atomize = atomize_conj ...;
2001-11-12 ago wenzelm val local_imp_def = thm "induct_implies_def";
2001-11-12 ago paulson ZF/Induct,UNITY
2001-11-12 ago paulson Tidying necessitated by new simprules in equalities.ML
2001-11-12 ago paulson conditional miniscoping equalities now made unconditional
2001-11-12 ago paulson new-style numerals without leading #, along with generic 0 and 1
2001-11-12 ago berghofe congc now returns None if congruence rule has no effect.
2001-11-12 ago berghofe Renamed some bound variables due to changes in simplifier.
2001-11-12 ago berghofe Fixed proof depending on strange behaviour of rename_bvs.
2001-11-12 ago berghofe Renamed some bound variables due to changes in simplifier.
2001-11-11 ago wenzelm present multi_result;
2001-11-11 ago wenzelm added meta_conjunction_tr';
2001-11-11 ago wenzelm pure_syntax_output: "_meta_conjunction";
2001-11-11 ago wenzelm adapted to multiple results;
2001-11-11 ago wenzelm adapted auto_bind_goal, auto_bind_facts;
2001-11-11 ago wenzelm added multi_theorem(_i);
2001-11-11 ago wenzelm Proof.have_i: multiple statements;
2001-11-11 ago wenzelm added RAW_METHOD, RAW_METHOD_CASES;
2001-11-11 ago wenzelm added add_thmss;
2001-11-11 ago wenzelm "theorem" etc.: multiple statements;
2001-11-11 ago wenzelm theorem, have, show etc: multiple statements;
2001-11-11 ago wenzelm facts: multiple args;
2001-11-11 ago wenzelm added conjunction_tac;
2001-11-11 ago wenzelm renamed open_smart_store_thms to smart_store_thms_open;
2001-11-11 ago wenzelm added mk_conjunction;
2001-11-11 ago wenzelm added unflat;
2001-11-11 ago wenzelm added conj_elim_precise, conj_intr_thm;
2001-11-10 ago wenzelm use Tactic.prove;
2001-11-09 ago wenzelm tuned;
2001-11-09 ago wenzelm support co/inductive definitions in new-style theories;
2001-11-09 ago wenzelm adapted to add_inductive_x;
2001-11-09 ago wenzelm syntactic declaration of external *and* internal versions of fixes;
2001-11-09 ago wenzelm fixed print_records;
2001-11-09 ago wenzelm tuned;
2001-11-09 ago wenzelm theorems case_split = case_split_thm [case_names True False, cases type: o];
2001-11-09 ago berghofe Theorems symmetric, reflexive and transitive are now stored with "open"
2001-11-09 ago berghofe Commands prf and full_prf can now also be used to display proof term
2001-11-09 ago wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
2001-11-09 ago wenzelm theory data: finish method;
2001-11-09 ago wenzelm indexvar_ast_tr (for \<index> placeholder);
2001-11-09 ago wenzelm removed pure_sym_syntax;
2001-11-09 ago wenzelm File.use;
2001-11-09 ago wenzelm added impose_hyps_tac;
2001-11-09 ago wenzelm proper close_locale;
2001-11-09 ago wenzelm no longer support "isabelle_font" or "symbols";
2001-11-09 ago wenzelm got rid of obsolete input filtering;
2001-11-09 ago wenzelm back to normal;
2001-11-09 ago wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
2001-11-09 ago wenzelm updated;
2001-11-09 ago wenzelm got rid of obsolete input filtering and isabelle font encoding;
2001-11-09 ago wenzelm got rid of obsolete input filtering;
2001-11-09 ago wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
2001-11-08 ago wenzelm theory data: finish method;
2001-11-08 ago wenzelm removed needs_filtered_use;
2001-11-08 ago wenzelm \newcommand{\isasymindex}{\isamath{\i}};
2001-11-08 ago wenzelm * Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,