2006-01-07 wenzelm 2006-01-07 added Isar/specification.ML;
2006-01-07 wenzelm 2006-01-07 updated;
2006-01-07 urbanc 2006-01-07 another change for the new induct-method
2006-01-07 wenzelm 2006-01-07 RuleCases.make_nested;
2006-01-07 wenzelm 2006-01-07 support nested cases; tuned apply_case;
2006-01-07 wenzelm 2006-01-07 support nested cases; added apply_case; replaced make/simple by make_common/nested/simple;
2006-01-07 wenzelm 2006-01-07 RuleCases.make_common;
2006-01-07 wenzelm 2006-01-07 pretty_locale: backquote notes;
2006-01-07 wenzelm 2006-01-07 RuleCases.make_simple;
2006-01-07 wenzelm 2006-01-07 tuned order;
2006-01-07 wenzelm 2006-01-07 added backquote;
2006-01-07 wenzelm 2006-01-07 RuleCases.make_common/nested;
2006-01-07 wenzelm 2006-01-07 * Provers/induct: improved simultaneous goals -- nested cases;
2006-01-07 urbanc 2006-01-07 added private datatype nprod (copy of prod) to be used in the induction rule
2006-01-07 urbanc 2006-01-07 changed PRO_RED proof to conform with the new induction rules
2006-01-06 wenzelm 2006-01-06 prep_meta_eq: reuse mk_rews of local simpset; adapted ML code to common conventions; tuned;
2006-01-06 wenzelm 2006-01-06 removed obsolete eqrule_HOL_data.ML;
2006-01-06 wenzelm 2006-01-06 removed obsolete eqrule_FOL_data.ML;
2006-01-06 wenzelm 2006-01-06 simplified EqSubst setup;
2006-01-06 wenzelm 2006-01-06 obsolete, reuse mk_rews of local simpset;
2006-01-06 wenzelm 2006-01-06 Toplevel.theory_to_proof;
2006-01-06 wenzelm 2006-01-06 transactions now always see quasi-functional intermediate checkpoint; removed obsolete theory_theory_to_proof; added
2006-01-06 wenzelm 2006-01-06 tuned EqSubst setup;
2006-01-06 wenzelm 2006-01-06 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
2006-01-05 wenzelm 2006-01-05 hide type datatype node; added theory_node, proof_node, is_theory, is_proof, proof_position_of, checkpoint, copy; no_body_context: no history; transaction: test save = true;
2006-01-05 wenzelm 2006-01-05 tuned print_theorems_theory;
2006-01-05 wenzelm 2006-01-05 Toplevel.proof_position_of;
2006-01-05 wenzelm 2006-01-05 store_thm: transfer to current context, i.e. the target theory;
2006-01-05 wenzelm 2006-01-05 replaced swap by contrapos_np;
2006-01-05 wenzelm 2006-01-05 added setminus; tuned;
2006-01-05 wenzelm 2006-01-05 proper handling of simultaneous goals and mutual rules;
2006-01-05 wenzelm 2006-01-05 provide projections of induct_weak, induct_unsafe;
2006-01-05 wenzelm 2006-01-05 added strict_mutual_rule;
2006-01-05 wenzelm 2006-01-05 RuleCases.strict_mutual_rule; export internalize;
2006-01-05 urbanc 2006-01-05 changed the name of the type "nOption" to "noption".
2006-01-04 urbanc 2006-01-04 added "fresh_singleton" lemma
2006-01-04 urbanc 2006-01-04 added more documentation; will now try out a modification of the ok-predicate
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2006-01-04 haftmann 2006-01-04 substantial additions using locales
2006-01-04 haftmann 2006-01-04 exported read|cert_arity interfaces
2006-01-04 nipkow 2006-01-04 trace_simp_depth_limit is 1 by default
2006-01-04 nipkow 2006-01-04 removed pointless trace msg.
2006-01-04 paulson 2006-01-04 preservation of names
2006-01-04 paulson 2006-01-04 a few more named lemmas
2006-01-04 haftmann 2006-01-04 fix: reintroduced pred_ctxt in gen_add_locale
2006-01-04 wenzelm 2006-01-04 tuned;
2006-01-04 wenzelm 2006-01-04 * Pure/Isar: Toplevel.theory_theory_to_proof;
2006-01-04 wenzelm 2006-01-04 added unlocalize_mfix;
2006-01-04 wenzelm 2006-01-04 added unlocalize_mixfix;
2006-01-04 wenzelm 2006-01-04 added theory_to_theory_to_proof, which may change theory before entering the proof; added forget_proof (from isar_thy.ML);
2006-01-04 wenzelm 2006-01-04 tuned;
2006-01-04 wenzelm 2006-01-04 moved forget_proof to toplevel.ML;
2006-01-04 wenzelm 2006-01-04 Toplevel.forget_proof;
2006-01-04 wenzelm 2006-01-04 adapted Toplevel.Proof;
2006-01-04 wenzelm 2006-01-04 removed dead code;
2006-01-04 wenzelm 2006-01-04 more stuff;
2006-01-03 paulson 2006-01-03 Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed
2006-01-03 paulson 2006-01-03 added explicit paths to required theories
2006-01-03 wenzelm 2006-01-03 added implementation manual;
2006-01-03 wenzelm 2006-01-03 more stuff;