Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/Pure/Isar/proof.ML
2006-11-28
wenzelm
2006-11-28
simplified '?' operator;
file
|
diff
|
annotate
2006-11-22
wenzelm
2006-11-22
init: enter inner statement mode, which prevents local notes from being named internally;
file
|
diff
|
annotate
2006-11-21
wenzelm
2006-11-21
made SML/NJ happy;
file
|
diff
|
annotate
2006-11-21
wenzelm
2006-11-21
removed obsolete simple_note_thms;
file
|
diff
|
annotate
2006-11-21
wenzelm
2006-11-21
simplified theorem(_i); notes: proper kind; renamed put_thms_internal to put_thms;
file
|
diff
|
annotate
2006-11-14
wenzelm
2006-11-14
simplified Proof.theorem(_i) interface -- removed target support; removed obsolete global_goal interface; removed goal_names, simplified goal kind output; tuned;
file
|
diff
|
annotate
2006-11-09
wenzelm
2006-11-09
Stack.map_top;
file
|
diff
|
annotate
2006-10-09
wenzelm
2006-10-09
def(_i): LocalDefs.add_defs; removed Drule.strip_shyps_warning;
file
|
diff
|
annotate
2006-10-07
wenzelm
2006-10-07
tuned;
file
|
diff
|
annotate
2006-08-09
wenzelm
2006-08-09
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
file
|
diff
|
annotate
2006-08-05
wenzelm
2006-08-05
removed obsolete sign_of;
file
|
diff
|
annotate
2006-08-02
wenzelm
2006-08-02
simplified Assumption/ProofContext.export; simplified end_block;
file
|
diff
|
annotate
2006-07-27
wenzelm
2006-07-27
moved basic assumption operations from structure ProofContext to Assumption;
file
|
diff
|
annotate
2006-07-26
wenzelm
2006-07-26
export goal_tac (was internal refine_tac);
file
|
diff
|
annotate
2006-07-06
wenzelm
2006-07-06
apply_text: support Method.Source_i;
file
|
diff
|
annotate
2006-07-04
wenzelm
2006-07-04
added schematic_goal;
file
|
diff
|
annotate
2006-06-17
wenzelm
2006-06-17
ProofContext.exports: simultaneous facts; Variable.exportT_terms;
file
|
diff
|
annotate
2006-06-15
wenzelm
2006-06-15
ProofContext: moved variable operations to struct Variable; tuned;
file
|
diff
|
annotate
2006-06-12
wenzelm
2006-06-12
Unify.matches_list;
file
|
diff
|
annotate
2006-06-11
wenzelm
2006-06-11
fixes: include mixfix syntax; goal: improved handling of implicit vars;
file
|
diff
|
annotate
2006-06-05
wenzelm
2006-06-05
allow non-trivial schematic goals (via embedded term vars);
file
|
diff
|
annotate
2006-05-07
wenzelm
2006-05-07
removed 'concl is' patterns;
file
|
diff
|
annotate
2006-04-27
wenzelm
2006-04-27
tuned basic list operators (flat, maps, map_filter);
file
|
diff
|
annotate
2006-04-26
wenzelm
2006-04-26
curried Seq.cons;
file
|
diff
|
annotate
2006-04-13
wenzelm
2006-04-13
use conjunction stuff from conjunction.ML;
file
|
diff
|
annotate
2006-03-21
wenzelm
2006-03-21
avoid polymorphic equality; subtract (op =);
file
|
diff
|
annotate
2006-03-08
wenzelm
2006-03-08
select_goals: split original conjunctions;
file
|
diff
|
annotate
2006-03-04
wenzelm
2006-03-04
method: SelectGoals;
file
|
diff
|
annotate
2006-02-17
wenzelm
2006-02-17
global_qeds: transfer body context;
file
|
diff
|
annotate
2006-02-16
wenzelm
2006-02-16
added put_thms_internal; tuned;
file
|
diff
|
annotate
2006-02-10
wenzelm
2006-02-10
tuned comment;
file
|
diff
|
annotate
2006-02-02
wenzelm
2006-02-02
added refine_insert;
file
|
diff
|
annotate
2006-01-31
wenzelm
2006-01-31
tuned LocalDefs.unfold;
file
|
diff
|
annotate
2006-01-29
wenzelm
2006-01-29
'unfolding': LocalDefs.unfold;
file
|
diff
|
annotate
2006-01-28
wenzelm
2006-01-28
LocalDefs; unfolding(_i): support object-level rewrites;
file
|
diff
|
annotate
2006-01-27
wenzelm
2006-01-27
swapped Toplevel.theory_context; tuned;
file
|
diff
|
annotate
2006-01-25
wenzelm
2006-01-25
ProofContext.export_standard;
file
|
diff
|
annotate
2006-01-21
wenzelm
2006-01-21
simplified type attribute;
file
|
diff
|
annotate
2006-01-14
wenzelm
2006-01-14
sane ERROR handling;
file
|
diff
|
annotate
2006-01-13
wenzelm
2006-01-13
uniform handling of fixes;
file
|
diff
|
annotate
2006-01-07
wenzelm
2006-01-07
RuleCases.make_common;
file
|
diff
|
annotate
2006-01-03
wenzelm
2006-01-03
added unfolding(_i); renamed using_thmss(_i) to using_i;
file
|
diff
|
annotate
2005-12-23
wenzelm
2005-12-23
goal/qed: proper treatment of two levels of conjunctions;
file
|
diff
|
annotate
2005-12-22
wenzelm
2005-12-22
auto cases: marked improper; tuned;
file
|
diff
|
annotate
2005-12-21
haftmann
2005-12-21
discontinued unflat in favour of burrow and burrow_split
file
|
diff
|
annotate
2005-12-09
haftmann
2005-12-09
oriented result pairs in PureThy
file
|
diff
|
annotate
2005-11-30
wenzelm
2005-11-30
simulaneous 'def';
file
|
diff
|
annotate
2005-11-22
wenzelm
2005-11-22
cases_tactic;
file
|
diff
|
annotate
2005-11-16
wenzelm
2005-11-16
ProofContext.mk_def;
file
|
diff
|
annotate
2005-11-08
wenzelm
2005-11-08
simplified after_qed;
file
|
diff
|
annotate
2005-10-28
wenzelm
2005-10-28
renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;
file
|
diff
|
annotate
2005-10-21
wenzelm
2005-10-21
export add_binds_i; invoke_case: AutoBind.no_facts; Goal.init, Goal.conclude;
file
|
diff
|
annotate
2005-10-18
wenzelm
2005-10-18
tuned error msg;
file
|
diff
|
annotate
2005-10-15
wenzelm
2005-10-15
goal statements: before_qed argument;
file
|
diff
|
annotate
2005-10-04
wenzelm
2005-10-04
minor tweaks for Poplog/ML;
file
|
diff
|
annotate
2005-09-17
wenzelm
2005-09-17
export put_facts; moved auto_fix to proof_context.ML; generic_goal: solve 0 subgoals initially; global_goal/theorem: only store results if SOME target, which may be empty;
file
|
diff
|
annotate
2005-09-16
ballarin
2005-09-16
interpretation uses primitive goal interface
file
|
diff
|
annotate
2005-09-13
wenzelm
2005-09-13
major cleanup of interfaces and implementation; generic goal commands: local/global_goal with after_qed; independent of locale.ML; more self-contained proof elements (material from isar_thy.ML); refer to ProofDisplay (cf. proof_display.ML); unified print_results (always normal); added get_thmss;
file
|
diff
|
annotate
2005-08-31
wenzelm
2005-08-31
refer to theory instead of low-level tsig;
file
|
diff
|
annotate
2005-08-28
wenzelm
2005-08-28
tuned;
file
|
diff
|
annotate