Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
moved debug option to proof_display.ML (again);
2006-08-02, by wenzelm
normalized Proof.context/method type aliases;
2006-08-02, by wenzelm
simplified Assumption/ProofContext.export;
2006-08-02, by wenzelm
added tactical result;
2006-08-02, by wenzelm
removed obsolete Drule.frees/vars_of etc.;
2006-08-02, by wenzelm
normalized Proof.context/method type aliases;
2006-08-02, by wenzelm
simplified Proof.end_block;
2006-08-02, by wenzelm
removed obsolete Drule.frees/vars_of etc.;
2006-08-02, by wenzelm
normalized Proof.context/method type aliases;
2006-08-02, by wenzelm
renamed Syntax.indexname to Syntax.read_indexname;
2006-08-02, by wenzelm
Variable.focus_subgoal;
2006-08-02, by wenzelm
replaced maxidx_of_proof by maxidx_proof;
2006-08-02, by wenzelm
prems-limit: int_option;
2006-08-02, by wenzelm
removed obsolete frees/vars_of etc.;
2006-08-02, by wenzelm
fake predeclaration of type Proof.context;
2006-08-02, by wenzelm
simplified export: no Seq.seq;
2006-08-02, by wenzelm
use proper RecdefPackage.get_hints;
2006-08-02, by wenzelm
removed obsolete Drule.frees/vars_of;
2006-08-02, by wenzelm
renamed thm_vars to thm_varnames;
2006-08-02, by wenzelm
removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
2006-08-02, by wenzelm
export get_hints;
2006-08-02, by wenzelm
normalized Proof.context/method type aliases;
2006-08-02, by wenzelm
normalized Proof.context/method type aliases;
2006-08-02, by wenzelm
simplified Assumption/ProofContext.export;
2006-08-02, by wenzelm
replaced obsolete standard/freeze_all by Variable.trade;
2006-08-02, by wenzelm
removed obsolete Drule.frees/vars_of etc.;
2006-08-02, by wenzelm
Added type constraint to please sml/nj
2006-08-02, by krauss
deleted obsolete file
2006-08-02, by paulson
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-08-02, by webertj
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-08-02, by webertj
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
2006-08-02, by mengj
type annotations fixed (IntInf.int, to make SML/NJ happy)
2006-08-02, by webertj
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-08-02, by webertj
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
2006-08-02, by webertj
comment (timing information for last example) added
2006-08-01, by webertj
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
2006-08-01, by webertj
removed skip
2006-08-01, by obua
Added in code to check too general axiom clauses.
2006-08-01, by mengj
exported attrib;
2006-08-01, by wenzelm
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-31, by webertj
fixed a bug in function poly: decomposition of products
2006-07-31, by webertj
Function package can now do automatic splits of overlapping datatype patterns
2006-07-31, by krauss
Removed an "apply arith" where there are already "No Subgoals"
2006-07-31, by krauss
code reformatted
2006-07-31, by webertj
Additional freshness constraints for FCB.
2006-07-31, by berghofe
proper Element.generalize_facts;
2006-07-30, by wenzelm
add_consts: proper Sign.full_name;
2006-07-30, by wenzelm
added generalize_facts;
2006-07-30, by wenzelm
added maxidx_values;
2006-07-30, by wenzelm
export: refrain from adjusting maxidx;
2006-07-30, by wenzelm
adjust_maxidx: pass explicit lower bound;
2006-07-30, by wenzelm
Thm.adjust_maxidx;
2006-07-30, by wenzelm
removed unused add_in_order/add_once (cf. OrdList.insert);
2006-07-30, by wenzelm
demod_rule: depend on context, proper Variable.import/export;
2006-07-30, by wenzelm
tuned proofs;
2006-07-30, by wenzelm
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-30, by webertj
bugfix related to cancel_div_mod simproc
2006-07-30, by webertj
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-29, by webertj
rename legacy_pretty_thm to pretty_thm_legacy;
2006-07-29, by wenzelm
tuned comment;
2006-07-29, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip