src/Pure/Isar/proof.ML
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;
2000-03-14 wenzelm 2000-03-14 invoke_case: include attributes;
2000-03-08 wenzelm 2000-03-08 invoke_case: name assumption;
2000-03-08 wenzelm 2000-03-08 generalized FINDGOAL, HEADGOAL; handling of local contexts: method_cases, invoke_case;
2000-02-14 wenzelm 2000-02-14 tuned msg;
2000-02-13 wenzelm 2000-02-13 refine_end;
2000-02-07 wenzelm 2000-02-07 assert_no_chain;
2000-02-02 wenzelm 2000-02-02 most_general_varify_tfrees all results;
2000-01-28 wenzelm 2000-01-28 added HEADGOAL;
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!); improved flexflex handling; tuned sig;
2000-01-05 wenzelm 2000-01-05 tuned;
1999-10-25 wenzelm 1999-10-25 improved handling of warn_extra_tfrees;
1999-10-22 wenzelm 1999-10-22 warn_extra_tfrees; removed bind(_i), add_binds, declare_term;
1999-09-30 wenzelm 1999-09-30 export find_free;