src/Pure/Isar/proof.ML
2001-12-19 wenzelm 2001-12-19 tuned interface of ProofContext.generalize; tuned;
2001-12-18 wenzelm 2001-12-18 use Locale.read/cert_context_statement;
2001-12-14 wenzelm 2001-12-14 tuned locale interface;
2001-12-14 wenzelm 2001-12-14 Locale.activate_context;
2001-12-08 wenzelm 2001-12-08 tuned print_state interfaces;
2001-11-28 wenzelm 2001-11-28 print_state: up to 7 result names;
2001-11-19 wenzelm 2001-11-19 improved treatment of common result name;
2001-11-19 wenzelm 2001-11-19 multi_theorem: common statement header (covers *all* results);
2001-11-16 wenzelm 2001-11-16 finish_global: Drule.strip_shyps_warning (just for warning);
2001-11-12 wenzelm 2001-11-12 empty rule_context for multiple goals;
2001-11-11 wenzelm 2001-11-11 added multi_theorem(_i); have, show etc.: multiple statements;
2001-11-07 wenzelm 2001-11-07 locale_prefix: Sign.base_name;
2001-11-06 wenzelm 2001-11-06 pretty_goals_local: observes context syntax; PureThy.store_thm: locale_prefix;
2001-11-06 wenzelm 2001-11-06 theorem(_i): locale atts; global_goal, finish_global: proper treatment of target locale;
2001-11-05 wenzelm 2001-11-05 pretty/print functions with context;
2001-11-04 wenzelm 2001-11-04 theorem(_i): locale elements;
2001-11-01 wenzelm 2001-11-01 theorem: locale argument;
2001-10-31 wenzelm 2001-10-31 theorem(_i): locale argument; contexts 0 and 1 in state now refer to theory and locale, respectively; unified export (no longer uses global "standard");
2001-10-31 berghofe 2001-10-31 Removed name_thm from finish_global.
2001-10-31 wenzelm 2001-10-31 finish_global: Tactic.norm_hhf;
2001-10-30 wenzelm 2001-10-30 tuned;
2001-10-24 wenzelm 2001-10-24 simplified ProofContext.assume interface;
2001-10-23 wenzelm 2001-10-23 moved RANGE to tctical.ML; moved export_assume, export_presume, export_def to proof_context.ML;
2001-10-23 wenzelm 2001-10-23 removed export_thm;
2001-10-22 wenzelm 2001-10-22 moved local defs to proof.ML (for locales);
2001-10-16 wenzelm 2001-10-16 simplified exporter interface;
2001-10-16 wenzelm 2001-10-16 support impromptu terminology of cases parameters;
2001-10-13 wenzelm 2001-10-13 generic theorem kinds;
2001-09-08 wenzelm 2001-09-08 print_state: subgoals;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-08-31 berghofe 2001-08-31 Tuned naming of theorems.
2001-02-07 wenzelm 2001-02-07 val get_goal: state -> context * (thm list * thm);
2001-01-18 wenzelm 2001-01-18 made SML/XL happy;
2001-01-18 wenzelm 2001-01-18 show(_i): check goal;
2001-01-09 wenzelm 2001-01-09 avoid renaming of params in cases;
2001-01-06 wenzelm 2001-01-06 moved norm_hhf_tac to Pure/tactic.ML; adapted invoke_case;
2000-11-30 wenzelm 2000-11-30 removed get_goal; suffer schematic (top-level) goals;
2000-11-21 wenzelm 2000-11-21 tag result with name reference to final binding (basically just a comment);
2000-11-13 wenzelm 2000-11-13 tuned statement args;
2000-11-10 wenzelm 2000-11-10 norm_hhf_tac;
2000-11-06 wenzelm 2000-11-06 RuleCases.make true;
2000-11-03 wenzelm 2000-11-03 tuned names;
2000-10-30 wenzelm 2000-10-30 tuned goals output;
2000-10-30 nipkow 2000-10-30 Added antiquotation "subgoals".
2000-10-24 wenzelm 2000-10-24 added pretty_goals;
2000-08-01 wenzelm 2000-08-01 tuned;
2000-07-30 wenzelm 2000-07-30 export RANGE, hard_asm_tac, soft_asm_tac; export is_chain, assert_forward_or_chain; added the_fact; updated ProofContext.export_wrt;
2000-07-13 wenzelm 2000-07-13 invoke_case: bind_skolem;
2000-06-29 wenzelm 2000-06-29 facts: handle multiple lists of arguments;
2000-05-28 wenzelm 2000-05-28 case 'antecedent';
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-17 wenzelm 2000-04-17 tuned msg;
2000-04-15 wenzelm 2000-04-15 next_block: reset_facts;
2000-04-05 wenzelm 2000-04-05 tuned comment;
2000-03-30 wenzelm 2000-03-30 support Hindley-Milner polymorphisms in binds and facts; let_bind(_i): polymorphic version; moved find_free, export_wrt to Isar/proof_context.ML;
2000-03-26 wenzelm 2000-03-26 tuned output;
2000-03-23 wenzelm 2000-03-23 tuned output;
2000-03-21 wenzelm 2000-03-21 soft_asm_tac: hack to norm goal;
2000-03-17 wenzelm 2000-03-17 next_block: allow in non-goal blocks as well (experimental);
2000-03-15 wenzelm 2000-03-15 pretty chunks;