#
4c3fdc06 |
|
09-Mar-2020 |
wenzelm <none@none> |
proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;
|
#
8c134e51 |
|
09-Mar-2020 |
wenzelm <none@none> |
tuned;
|
#
3eb980f3 |
|
09-Mar-2020 |
wenzelm <none@none> |
tuned whitespace;
|
#
741cf868 |
|
09-Mar-2020 |
wenzelm <none@none> |
clarified;
|
#
e576a429 |
|
09-Mar-2020 |
wenzelm <none@none> |
tuned signature;
|
#
a6213100 |
|
24-Feb-2020 |
wenzelm <none@none> |
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
|
#
522ea636 |
|
04-Nov-2019 |
wenzelm <none@none> |
uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes;
|
#
6c3bc8cf |
|
04-Nov-2019 |
wenzelm <none@none> |
more robust expose_proofs corresponding to register_proofs/consolidate_theory; expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context;
|
#
7474525a |
|
03-Nov-2019 |
wenzelm <none@none> |
clarified signature -- more options;
|
#
a87dae10 |
|
02-Nov-2019 |
wenzelm <none@none> |
proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);
|
#
4be542d9 |
|
01-Nov-2019 |
wenzelm <none@none> |
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
|
#
95ad9502 |
|
02-Nov-2019 |
wenzelm <none@none> |
clarified signature;
|
#
8b58f18a |
|
01-Nov-2019 |
wenzelm <none@none> |
clarified signature (again);
|
#
22873e75 |
|
01-Nov-2019 |
wenzelm <none@none> |
clarified signature;
|
#
9c1d4bf1 |
|
01-Nov-2019 |
wenzelm <none@none> |
make double-sure that internal proof boxes are exported, e.g. in Pure;
|
#
b84c6f63 |
|
01-Nov-2019 |
wenzelm <none@none> |
clarified modules (again);
|
#
2623fb27 |
|
01-Nov-2019 |
wenzelm <none@none> |
more detailed proof term output; tuned signature;
|
#
ea088b3c |
|
01-Nov-2019 |
wenzelm <none@none> |
tuned signature;
|
#
91d83298 |
|
31-Oct-2019 |
wenzelm <none@none> |
more accurate proof_boxes -- from actual proof body;
|
#
1df29765 |
|
26-Oct-2019 |
wenzelm <none@none> |
proper order of variables, independently of varify/unvarify state -- relevant for export of locale conclusions;
|
#
e17e9363 |
|
20-Oct-2019 |
wenzelm <none@none> |
clarified signature: name of standard_proof is authentic, otherwise empty;
|
#
55dce9a0 |
|
20-Oct-2019 |
wenzelm <none@none> |
clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format;
|
#
0e936e0a |
|
19-Oct-2019 |
wenzelm <none@none> |
export toplevel proof similar to named PThm;
|
#
70fb43ac |
|
19-Oct-2019 |
wenzelm <none@none> |
tuned signature;
|
#
d4d09e6e |
|
17-Oct-2019 |
wenzelm <none@none> |
turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;
|
#
140b0d83 |
|
17-Oct-2019 |
wenzelm <none@none> |
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
|
#
9553c1f0 |
|
17-Oct-2019 |
wenzelm <none@none> |
clarified proof_boxes (requires prune_proofs=false);
|
#
8ec9e325 |
|
16-Oct-2019 |
wenzelm <none@none> |
more robust: avoid looping Lazy.force due to misinterpreted interrupt;
|
#
85d89a9e |
|
16-Oct-2019 |
wenzelm <none@none> |
more informative combination_proof, e.g. relevant for proper type inference in HOL.Product_Type (with export_proofs);
|
#
b67e6c9b |
|
16-Oct-2019 |
wenzelm <none@none> |
tuned -- more stable type inference;
|
#
f42e395d |
|
15-Oct-2019 |
wenzelm <none@none> |
more support for proof terms; clarified signature;
|
#
e4654768 |
|
15-Oct-2019 |
wenzelm <none@none> |
clarified proof export;
|
#
007ee8b7 |
|
15-Oct-2019 |
wenzelm <none@none> |
skip (somewhat pointless) shrink_proof more uniformly;
|
#
d5713c0a |
|
15-Oct-2019 |
wenzelm <none@none> |
apply_preproc for all proof boxes;
|
#
b683d8b0 |
|
12-Oct-2019 |
wenzelm <none@none> |
support preprocessing of exported proofs;
|
#
61e80d14 |
|
12-Oct-2019 |
wenzelm <none@none> |
more compact XML;
|
#
06c84f7f |
|
12-Oct-2019 |
wenzelm <none@none> |
more compact XML: separate environment for free variables; clarified fold_proof_terms vs. fold_proof_terms_types;
|
#
2d7677d5 |
|
11-Oct-2019 |
wenzelm <none@none> |
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
|
#
224886d1 |
|
11-Oct-2019 |
wenzelm <none@none> |
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
|
#
0ba6f50c |
|
11-Oct-2019 |
wenzelm <none@none> |
clarified oracle_proof;
|
#
bfbc58d6 |
|
11-Oct-2019 |
wenzelm <none@none> |
tuned;
|
#
05321d7f |
|
11-Oct-2019 |
wenzelm <none@none> |
tuned;
|
#
cdb9bd9e |
|
11-Oct-2019 |
wenzelm <none@none> |
tuned;
|
#
5954cb84 |
|
11-Oct-2019 |
wenzelm <none@none> |
clarified signature;
|
#
d659b0d2 |
|
11-Oct-2019 |
wenzelm <none@none> |
tuned signature;
|
#
0dd11192 |
|
10-Oct-2019 |
wenzelm <none@none> |
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
|
#
718c279c |
|
10-Oct-2019 |
wenzelm <none@none> |
clarified modules;
|
#
8eb7c22a |
|
10-Oct-2019 |
wenzelm <none@none> |
tuned whitespace;
|
#
821213fd |
|
10-Oct-2019 |
wenzelm <none@none> |
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
|
#
a37070e2 |
|
09-Oct-2019 |
wenzelm <none@none> |
tuned;
|
#
af3bddc4 |
|
09-Oct-2019 |
wenzelm <none@none> |
misc tuning and clarification;
|
#
fc7b6d83 |
|
09-Oct-2019 |
wenzelm <none@none> |
clarified signature -- some operations to support fully explicit proof terms;
|
#
411b259a |
|
08-Oct-2019 |
wenzelm <none@none> |
tuned;
|
#
3535630a |
|
08-Oct-2019 |
wenzelm <none@none> |
tuned;
|
#
e5acb291 |
|
08-Oct-2019 |
wenzelm <none@none> |
proper treatment of sorts;
|
#
7391b61e |
|
08-Oct-2019 |
wenzelm <none@none> |
tuned app_types: more direct map_proof_types_same;
|
#
3dbd8fa2 |
|
04-Oct-2019 |
wenzelm <none@none> |
Term_XML.Encode/Decode.term uses Const "typargs";
|
#
4d7de99d |
|
23-Aug-2019 |
wenzelm <none@none> |
more compact: avoid pointless PThm rudiments;
|
#
d2124da3 |
|
23-Aug-2019 |
wenzelm <none@none> |
clarified signature: prefer total operations;
|
#
19fa1d88 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified thm_id vs. thm_node/thm: retain theory_name; support for thm_deps: expand unnamed nodes;
|
#
3b572107 |
|
20-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
22a4d5e3 |
|
20-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
c7c2b0a9 |
|
20-Aug-2019 |
wenzelm <none@none> |
tuned signature;
|
#
575c191f |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified modules;
|
#
d04c6e3d |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified modules;
|
#
7d08d36e |
|
20-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
438cc573 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
b97e0898 |
|
19-Aug-2019 |
wenzelm <none@none> |
tuned signature;
|
#
80c8e4b8 |
|
19-Aug-2019 |
wenzelm <none@none> |
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
|
#
359888d7 |
|
19-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
d29de9af |
|
17-Aug-2019 |
wenzelm <none@none> |
discontinued peek_status: unused and not clearly defined;
|
#
f55c44db |
|
17-Aug-2019 |
wenzelm <none@none> |
more robust, notably for open_proof of unnamed derivation;
|
#
a8d425ee |
|
17-Aug-2019 |
wenzelm <none@none> |
clarified type for recorded oracles;
|
#
e8e538ec |
|
17-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
2a1a9b9c |
|
17-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
67b67048 |
|
16-Aug-2019 |
wenzelm <none@none> |
clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;
|
#
0245bd29 |
|
15-Aug-2019 |
wenzelm <none@none> |
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
|
#
85489698 |
|
15-Aug-2019 |
wenzelm <none@none> |
more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
|
#
cbd5363d |
|
15-Aug-2019 |
wenzelm <none@none> |
clarified PThm: theory_name simplifies retrieval from exports;
|
#
92acb5ae |
|
15-Aug-2019 |
wenzelm <none@none> |
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
|
#
f36251c5 |
|
14-Aug-2019 |
wenzelm <none@none> |
clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);
|
#
7f6bf383 |
|
14-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
0f4ea675 |
|
14-Aug-2019 |
wenzelm <none@none> |
uniform standard_vars for terms and proof terms;
|
#
e488582f |
|
12-Aug-2019 |
wenzelm <none@none> |
tuned -- eliminated unused parameters;
|
#
112a47e0 |
|
12-Aug-2019 |
wenzelm <none@none> |
more direct/compact export of proof terms;
|
#
440eb01a |
|
10-Aug-2019 |
wenzelm <none@none> |
more careful export of unnamed proof boxes: avoid duplicates via memoing;
|
#
2085ca01 |
|
10-Aug-2019 |
wenzelm <none@none> |
tuned signature;
|
#
81c452ae |
|
10-Aug-2019 |
wenzelm <none@none> |
export each PThm node separately: slightly more scalable;
|
#
5784f297 |
|
10-Aug-2019 |
wenzelm <none@none> |
more positions;
|
#
573204f4 |
|
09-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
#
9a7bc12a |
|
09-Aug-2019 |
wenzelm <none@none> |
clarified ML types;
|
#
a51d5014 |
|
09-Aug-2019 |
wenzelm <none@none> |
proper treatment of body oracles, outside of recursion into thms graph;
|
#
e91e3ab4 |
|
02-Aug-2019 |
wenzelm <none@none> |
more direct proofs for type classes; misc tuning and cleanup;
|
#
c24dd438 |
|
01-Aug-2019 |
wenzelm <none@none> |
clarified module structure;
|
#
f8fc9859 |
|
31-Jul-2019 |
wenzelm <none@none> |
clarified export: retain proof boxes as local definitions -- more scalable;
|
#
cc49f21e |
|
30-Jul-2019 |
wenzelm <none@none> |
clarified global theory context;
|
#
c1bd1263 |
|
30-Jul-2019 |
wenzelm <none@none> |
more robust export, based on reconstruct_proof / expand_proof;
|
#
bec922a7 |
|
30-Jul-2019 |
wenzelm <none@none> |
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
|
#
eb10a539 |
|
30-Jul-2019 |
wenzelm <none@none> |
discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;
|
#
b8350b7b |
|
29-Jul-2019 |
wenzelm <none@none> |
more diagnostic operations;
|
#
29fe913e |
|
29-Jul-2019 |
wenzelm <none@none> |
tuned -- non-strict args;
|
#
54e159a9 |
|
29-Jul-2019 |
wenzelm <none@none> |
tuned signature;
|
#
24be7acc |
|
29-Jul-2019 |
wenzelm <none@none> |
clarified signature; tuned;
|
#
752574b8 |
|
29-Jul-2019 |
wenzelm <none@none> |
tuned signature;
|
#
e9daa8ef |
|
27-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
1eb8b82f |
|
27-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
380d9085 |
|
26-Jul-2019 |
wenzelm <none@none> |
tuned -- reorder sections;
|
#
71260b45 |
|
26-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
5a9e311d |
|
26-Jul-2019 |
wenzelm <none@none> |
tuned signature;
|
#
b9704753 |
|
26-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
0133595b |
|
26-Jul-2019 |
wenzelm <none@none> |
finalize proofs earlier to reduce memory requirement;
|
#
2b3d7e3b |
|
26-Jul-2019 |
wenzelm <none@none> |
more explicit type proof_serial;
|
#
e1232d26 |
|
26-Jul-2019 |
wenzelm <none@none> |
defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement; misc tuning and clarification;
|
#
d74673da |
|
24-Jul-2019 |
wenzelm <none@none> |
prefer local counter;
|
#
2278dcf3 |
|
24-Jul-2019 |
wenzelm <none@none> |
more accurate proof export;
|
#
989c12b6 |
|
24-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
e5788004 |
|
24-Jul-2019 |
wenzelm <none@none> |
more thorough clean_proof;
|
#
049731d8 |
|
23-Jul-2019 |
wenzelm <none@none> |
treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
|
#
005eebf0 |
|
23-Jul-2019 |
wenzelm <none@none> |
clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named; added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;
|
#
2c6c6e73 |
|
22-Jul-2019 |
wenzelm <none@none> |
tuned comments;
|
#
6ce0a4e1 |
|
22-Jul-2019 |
wenzelm <none@none> |
proof terms are always constructed sequentially; discontinued unused Proofterm.Promise -- too complex;
|
#
bf5e3cea |
|
22-Jul-2019 |
wenzelm <none@none> |
tuned comments -- proper sections;
|
#
7f034abf |
|
22-Jul-2019 |
wenzelm <none@none> |
support export_proofs, prune_proofs; tuned comments;
|
#
39636472 |
|
22-Jul-2019 |
wenzelm <none@none> |
clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
|
#
3eeb771c |
|
22-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
4bcf4780 |
|
22-Jul-2019 |
wenzelm <none@none> |
clarified exception;
|
#
d5b83362 |
|
22-Jul-2019 |
wenzelm <none@none> |
tuned;
|
#
ced23f10 |
|
22-Jul-2019 |
wenzelm <none@none> |
more accurate type information;
|
#
fe9eef5c |
|
21-Jul-2019 |
wenzelm <none@none> |
global declaration of abstract syntax for proof terms, with qualified names; clarified modules;
|
#
5b240aad |
|
02-May-2018 |
wenzelm <none@none> |
tuned -- slightly smaller future closure size;
|
#
95633a2b |
|
24-Apr-2018 |
wenzelm <none@none> |
more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;
|
#
21b009db |
|
24-Apr-2018 |
wenzelm <none@none> |
less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);
|
#
8d13ec89 |
|
19-Feb-2018 |
wenzelm <none@none> |
tuned: more parallel;
|
#
f30be3c8 |
|
22-Jun-2017 |
wenzelm <none@none> |
consolidate proofs more simultaneously;
|
#
ee8a0899 |
|
22-Jun-2017 |
wenzelm <none@none> |
more informative task_statistics;
|
#
4a167caa |
|
09-Apr-2017 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
0166ce0c |
|
16-Dec-2016 |
wenzelm <none@none> |
consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;
|
#
bb08a577 |
|
16-Dec-2016 |
wenzelm <none@none> |
tuned signature -- more abstract type thm_node;
|
#
cec9b978 |
|
15-Dec-2016 |
wenzelm <none@none> |
tuned signature;
|
#
e33b0cb4 |
|
14-Dec-2016 |
wenzelm <none@none> |
more careful derivation_closed / close_derivation;
|
#
f5251071 |
|
14-Dec-2016 |
wenzelm <none@none> |
tuned whitespace;
|
#
bd6cb4fe |
|
12-Sep-2016 |
wenzelm <none@none> |
tuned -- fewer warnings;
|
#
194058d8 |
|
06-Aug-2016 |
wenzelm <none@none> |
tuned signature;
|
#
8ec93140 |
|
06-Apr-2016 |
wenzelm <none@none> |
prefer regular context update, to allow continuous editing of Pure;
|
#
56f8495e |
|
08-Mar-2016 |
haftmann <none@none> |
provide explicit hint concering uniqueness of derivation
|
#
54f4e638 |
|
23-Mar-2015 |
wenzelm <none@none> |
local fixes may depend on goal params;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
f9d3edb3 |
|
18-Jul-2013 |
wenzelm <none@none> |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
#
87953653 |
|
30-Jun-2013 |
wenzelm <none@none> |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
#
b628a60a |
|
27-Jun-2013 |
wenzelm <none@none> |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
#
282faa2e |
|
23-Jun-2013 |
wenzelm <none@none> |
support for XML data representation of proof terms;
|
#
cba98832 |
|
12-Apr-2013 |
wenzelm <none@none> |
tuned signature; tuned comments;
|
#
bec8f891 |
|
13-Feb-2013 |
wenzelm <none@none> |
discontinued home-made sharing for proof terms -- leave memory management to the Poly/ML RTS;
|
#
4d22191f |
|
24-Jan-2013 |
wenzelm <none@none> |
avoid extra fork for fulfill_proof_future whenever possible -- without proof terms it merely doubles the number of proof tasks redundantly, by piggy-backing another 10 microseconds task;
|
#
5afc569b |
|
07-Jan-2013 |
wenzelm <none@none> |
no fork from draft thy -- avoid potential for crash via classrel_proof/arity_proof;
|
#
21db81be |
|
19-Nov-2012 |
wenzelm <none@none> |
theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
|
#
c36c4f6a |
|
16-Oct-2011 |
wenzelm <none@none> |
added Term.dummy_pattern conveniences;
|
#
11f92502 |
|
20-Aug-2011 |
wenzelm <none@none> |
more direct balanced version Ord_List.unions;
|
#
40f65ac9 |
|
20-Aug-2011 |
wenzelm <none@none> |
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
|
#
79290f18 |
|
20-Aug-2011 |
wenzelm <none@none> |
tuned future priorities (again);
|
#
43f68989 |
|
20-Aug-2011 |
wenzelm <none@none> |
clarified fulfill_norm_proof: no join_thms yet; clarified priority of fulfill_proof_future, which is followed by explicit join_thms; explicit Thm.future_body_of without join yet; tuned Thm.future_result: join_promises without fulfill_norm_proof;
|
#
b712c530 |
|
20-Aug-2011 |
wenzelm <none@none> |
added Future.joins convenience; clarified Future.map: based on Future.cond_forks;
|
#
cc056f00 |
|
19-Aug-2011 |
wenzelm <none@none> |
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
|
#
94c87949 |
|
19-Aug-2011 |
wenzelm <none@none> |
tuned;
|
#
c810f9c3 |
|
10-Aug-2011 |
wenzelm <none@none> |
avoid OldTerm operations -- with subtle changes of semantics;
|
#
0b684231 |
|
10-Aug-2011 |
wenzelm <none@none> |
avoid OldTerm operations -- with subtle changes of semantics;
|
#
8c3c55ef |
|
10-Aug-2011 |
wenzelm <none@none> |
future_job: explicit indication of interrupts;
|
#
e261188b |
|
09-Aug-2011 |
wenzelm <none@none> |
misc tuning and clarification;
|
#
88bb35a0 |
|
09-Aug-2011 |
wenzelm <none@none> |
tuned whitespace;
|
#
ef30167b |
|
13-Jul-2011 |
wenzelm <none@none> |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
#
25118ed6 |
|
11-Jul-2011 |
wenzelm <none@none> |
tuned signature -- corresponding to Scala version;
|
#
b6f9ad57 |
|
09-Jun-2011 |
wenzelm <none@none> |
tuned signature: Name.invent and Name.invent_names;
|
#
1a5a42ee |
|
09-Jun-2011 |
wenzelm <none@none> |
simplified Name.variant -- discontinued builtin fold_map;
|
#
ec1196d6 |
|
09-Jun-2011 |
wenzelm <none@none> |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
#
390ebc4a |
|
08-Jun-2011 |
wenzelm <none@none> |
more robust exception pattern General.Subscript;
|
#
17eb06fd |
|
03-Feb-2011 |
wenzelm <none@none> |
tuned comments;
|
#
4822c144 |
|
03-Feb-2011 |
wenzelm <none@none> |
clarified Proofterm.proofs_enabled;
|
#
ea3105a6 |
|
31-Jan-2011 |
wenzelm <none@none> |
tuned signature; tuned vacous forks;
|
#
dbeb61d4 |
|
31-Jan-2011 |
wenzelm <none@none> |
support named tasks, for improved tracing;
|
#
a6997b1f |
|
31-Jan-2011 |
wenzelm <none@none> |
more direct Future.bulk, which potentially reduces overhead for Par_List; tuned signature;
|
#
86bc1118 |
|
24-Sep-2010 |
wenzelm <none@none> |
modernized structure Ord_List;
|
#
9e2201a3 |
|
01-Sep-2010 |
haftmann <none@none> |
replaced Table.map' by Table.map
|
#
d8a8dc0a |
|
02-Jun-2010 |
wenzelm <none@none> |
always unconstrain thm proofs;
|
#
d7f009d2 |
|
02-Jun-2010 |
wenzelm <none@none> |
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
|
#
631b5f8e |
|
01-Jun-2010 |
berghofe <none@none> |
- outer_constraints with original variable names, to ensure that argsP is consistent with args - Exported map_proof_same, added implies_intr_proof' and forall_intr_proof' - Rewriting procedures used by rewrite_proof can now access hypotheses - Finally enabled unconstrain
|
#
c25c5530 |
|
31-May-2010 |
wenzelm <none@none> |
modernized some structure names, keeping a few legacy aliases;
|
#
b38bc499 |
|
14-May-2010 |
wenzelm <none@none> |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
#
f31a5582 |
|
13-May-2010 |
wenzelm <none@none> |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
#
b4ca11a6 |
|
13-May-2010 |
wenzelm <none@none> |
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
|
#
3bc9c5b2 |
|
13-May-2010 |
wenzelm <none@none> |
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
|
#
2d596675 |
|
13-May-2010 |
wenzelm <none@none> |
unconstrainT operations on proofs, according to krauss/schropp;
|
#
2901f9d1 |
|
13-May-2010 |
wenzelm <none@none> |
added Proofterm.get_name variants according to krauss/schropp; tuned signature;
|
#
e3aceea5 |
|
08-May-2010 |
wenzelm <none@none> |
tuned signature;
|
#
9adf3e5b |
|
08-May-2010 |
wenzelm <none@none> |
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
|
#
657d0cdf |
|
08-May-2010 |
wenzelm <none@none> |
back-patching of axclass proofs;
|
#
34ec8df5 |
|
07-May-2010 |
wenzelm <none@none> |
strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
|
#
5e89d7bc |
|
04-May-2010 |
wenzelm <none@none> |
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences: * present type variables are only compared wrt. first component (the atomic type), not the duplicated sort; * extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem); * deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;
|
#
2f4d80c9 |
|
03-May-2010 |
wenzelm <none@none> |
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
|
#
260d4e35 |
|
04-May-2010 |
wenzelm <none@none> |
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
|
#
ddeb6549 |
|
21-Mar-2010 |
wenzelm <none@none> |
do not open ML structures;
|
#
bbc8cf56 |
|
20-Mar-2010 |
wenzelm <none@none> |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
#
e3d0611a |
|
27-Feb-2010 |
wenzelm <none@none> |
modernized structure Term_Ord;
|
#
02c48bf5 |
|
25-Nov-2009 |
haftmann <none@none> |
normalized uncurry take/drop --HG-- extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9
|
#
e3772a5e |
|
24-Nov-2009 |
haftmann <none@none> |
curried take/drop --HG-- extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0
|
#
f5084a96 |
|
16-Nov-2009 |
wenzelm <none@none> |
generalized procs for rewrite_proof: allow skeleton; fulfill_norm_proof: always normalize result here, no re-normalization after filling;
|
#
71833c27 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Theory_Data; tuned;
|
#
cbf1e6f5 |
|
04-Nov-2009 |
wenzelm <none@none> |
revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
|
#
f184d52a |
|
04-Nov-2009 |
wenzelm <none@none> |
fulfill_proof_future: tuned important special case of singleton promise;
|
#
d0106d17 |
|
29-Oct-2009 |
wenzelm <none@none> |
standardized filter/filter_out;
|
#
26a442f9 |
|
20-Oct-2009 |
haftmann <none@none> |
curried union as canonical list operation
|
#
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
#
68478f6d |
|
20-Oct-2009 |
haftmann <none@none> |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
#
8256bde7 |
|
01-Oct-2009 |
wenzelm <none@none> |
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
|
#
f7c550fb |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated redundant parameters;
|
#
b9d789f1 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
#
a9b50ad4 |
|
28-Sep-2009 |
wenzelm <none@none> |
fold_body_thms: pass pthm identifier; fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen"; fulfill_proof/thm_proof: check for thm cycles at the substitution point;
|
#
c102a955 |
|
27-Sep-2009 |
wenzelm <none@none> |
fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
|
#
6af3c4e3 |
|
24-Jul-2009 |
wenzelm <none@none> |
get_name: cover only PThm, not PAxm;
|
#
04f604b2 |
|
21-Jul-2009 |
wenzelm <none@none> |
prefer simultaneous join -- for improved scheduling;
|
#
9905c732 |
|
19-Jul-2009 |
wenzelm <none@none> |
tuned;
|
#
ba9b4c09 |
|
18-Jul-2009 |
wenzelm <none@none> |
added join_bodies;
|
#
3a8a14e2 |
|
17-Jul-2009 |
wenzelm <none@none> |
tuned prf_subst: use structure Same;
|
#
d9aef710 |
|
17-Jul-2009 |
wenzelm <none@none> |
tuned/modernized Envir.subst_XXX;
|
#
e895af14 |
|
17-Jul-2009 |
wenzelm <none@none> |
tuned/modernized Envir operations;
|
#
a42516d9 |
|
16-Jul-2009 |
wenzelm <none@none> |
tuned incr_indexes;
|
#
46eeb15b |
|
16-Jul-2009 |
wenzelm <none@none> |
tuned map_proof_terms_option; eliminated apsome, apsome'; tuned;
|
#
8e108ac5 |
|
16-Jul-2009 |
wenzelm <none@none> |
use structure Same; do not open Envir;
|
#
196435a0 |
|
09-Jul-2009 |
wenzelm <none@none> |
renamed structure TermSubst to Term_Subst;
|
#
2bcff546 |
|
06-Jul-2009 |
wenzelm <none@none> |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
#
968dc814 |
|
02-Jul-2009 |
wenzelm <none@none> |
added pro-forma proof constructor Inclass;
|
#
61637bb8 |
|
25-Mar-2009 |
wenzelm <none@none> |
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof; added approximate_proof_body -- replaces former make_proof_body; added all_oracles_of; oracle_proof: explicit oracle result; fulfill_proof/thm_proof: require proper proof_body futures, to maintain full account of oracles and thms (repairs a serious problem of the old version);
|
#
00220a36 |
|
24-Mar-2009 |
wenzelm <none@none> |
status_of: simultaneous list;
|
#
6a79c913 |
|
24-Mar-2009 |
wenzelm <none@none> |
display derivation status of thms;
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
2a1579cf |
|
27-Feb-2009 |
wenzelm <none@none> |
eliminated NJ's List.nth;
|
#
def8eba06 |
|
27-Jan-2009 |
wenzelm <none@none> |
thm_proof: recovered single-threaded version;
|
#
d9512627 |
|
26-Jan-2009 |
wenzelm <none@none> |
thm_proof: replaced lazy by composed futures;
|
#
aab2e86d |
|
26-Jan-2009 |
wenzelm <none@none> |
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
|
#
1be33ad4 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
#
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
|
#
b88342b6 |
|
30-Dec-2008 |
wenzelm <none@none> |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
#
0eb1e547 |
|
30-Dec-2008 |
wenzelm <none@none> |
freeze_thaw: canonical Term.add_XXX operations; varify: regular name context;
|
#
ef025228 |
|
04-Dec-2008 |
wenzelm <none@none> |
renamed type Lazy.T to lazy;
|
#
de523228 |
|
23-Nov-2008 |
wenzelm <none@none> |
tuned;
|
#
5474ba15 |
|
23-Nov-2008 |
wenzelm <none@none> |
eliminated finish_proof, keep pre/post normalization of results separate;
|
#
cdb83469 |
|
18-Nov-2008 |
wenzelm <none@none> |
fulfill_proof/thm_proof: commuted lazyness;
|
#
24a8dfef |
|
17-Nov-2008 |
wenzelm <none@none> |
finish_proof: undefined promises may occur here;
|
#
94576c0b |
|
17-Nov-2008 |
wenzelm <none@none> |
unified treatment of PAxm/Oracle/Promise in basic proof term operations; refined promise/fulfill: maintain proper type instantiation, disallow term variables; thm_proof: uniform finish_proof before and after fulfill;
|
#
61ec1ace |
|
16-Nov-2008 |
wenzelm <none@none> |
proof_body/pthm: removed redundant types field; fold_proof_atoms: unified recursive case with fold_body_thms; tuned signature;
|
#
2d855682 |
|
16-Nov-2008 |
berghofe <none@none> |
Frees in PThms are now quantified in the order of their appearance in the proposition as well, to make it compatible (again) with variable order used by forall_intr_frees.
|
#
c2636b4c |
|
15-Nov-2008 |
wenzelm <none@none> |
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial); added type proof_body, which covers oracles and thms of local proof; added general fold_body_thms, fold_proof_atoms; removed thms_of_proof, thms_of_proof', axms_of_proof; slightly more abstract handling of body content (oracles, thms); rewrite_proof: simplified simprocs (no name required); thm_proof: lazy fulfillment of promises;
|
#
a1ccf296 |
|
23-Sep-2008 |
wenzelm <none@none> |
added conditional add_oracles, keep oracles_of_proof private; added fulfill; removed unused is_named; tuned some table operations;
|
#
158f2d53 |
|
22-Sep-2008 |
wenzelm <none@none> |
added Promise constructor, which is similar to Oracle but may be replaced later; added promise_proof; export min_proof, mk_min_proof; moved infer_derivs to thm.ML as derive_rule0/1/2; tuned oracles_of_proof; added is_named;
|
#
eeba5bb1 |
|
23-Jun-2008 |
wenzelm <none@none> |
Logic.all/mk_equals/mk_implies;
|
#
ebfb5671 |
|
12-Apr-2008 |
wenzelm <none@none> |
rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;
|
#
a6067101 |
|
27-Mar-2008 |
wenzelm <none@none> |
eliminated theory ProtoPure;
|
#
7e0b4be6 |
|
19-Mar-2008 |
haftmann <none@none> |
Type.lookup now curried
|
#
92b97cae |
|
11-Jul-2007 |
berghofe <none@none> |
Added function rew_proof (for pre-normalizing proofs).
|
#
aac77467 |
|
08-Jun-2007 |
berghofe <none@none> |
Adapted Proofterm.bicompose_proof to Larry's changes in Logic.assum_pairs from 2005-01-24 (revision 1.44).
|
#
ca14c530 |
|
31-May-2007 |
wenzelm <none@none> |
simplified/unified list fold;
|
#
b62fe892 |
|
06-May-2007 |
wenzelm <none@none> |
simplified DataFun interfaces;
|
#
2781c77f |
|
13-Apr-2007 |
haftmann <none@none> |
canonical merge operations
|
#
b5dac97b |
|
04-Dec-2006 |
wenzelm <none@none> |
thm/prf: separate official name vs. additional tags;
|
#
1c390ba8 |
|
04-Oct-2006 |
haftmann <none@none> |
*** empty log message ***
|
#
e69dd782 |
|
15-Sep-2006 |
wenzelm <none@none> |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
#
b6b974b5 |
|
11-Sep-2006 |
wenzelm <none@none> |
moved term subst functions to TermSubst;
|
#
1102e46e |
|
02-Aug-2006 |
wenzelm <none@none> |
replaced maxidx_of_proof by maxidx_proof;
|
#
1cdf1137 |
|
18-Jul-2006 |
wenzelm <none@none> |
tuned;
|
#
e59a8ced |
|
18-Jul-2006 |
wenzelm <none@none> |
fold_proof_terms: canonical arguments; removed obsolete add_prf_names, add_prf_tfree_names, add_prf_tvar_ixns;
|
#
35141c3c |
|
10-Jul-2006 |
wenzelm <none@none> |
replaced Term.variant(list) by Name.variant(_list);
|
#
7787a399 |
|
04-Jul-2006 |
wenzelm <none@none> |
added map_proof_terms_option; tuned generalize, instantiate;
|
#
ae7adafd |
|
17-Jun-2006 |
wenzelm <none@none> |
added generalize rule;
|
#
44d31bf2 |
|
29-Apr-2006 |
wenzelm <none@none> |
tuned;
|
#
cf09f0e2 |
|
27-Apr-2006 |
wenzelm <none@none> |
tuned basic list operators (flat, maps, map_filter);
|
#
e9668ee4 |
|
07-Apr-2006 |
berghofe <none@none> |
Added alternative version of thms_of_proof that does not recursively descend into proofs of (named) theorems.
|
#
5e7143ec |
|
20-Mar-2006 |
wenzelm <none@none> |
remove (op =); tuned;
|
#
d4f142f8 |
|
08-Mar-2006 |
wenzelm <none@none> |
infer_derivs: avoid allocating empty MinProof;
|
#
6bee66ba |
|
11-Feb-2006 |
wenzelm <none@none> |
tuned;
|
#
13808884 |
|
06-Feb-2006 |
haftmann <none@none> |
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
|
#
aabb579b |
|
21-Dec-2005 |
wenzelm <none@none> |
bicompose_proof: no_flatten;
|
#
7cec4705 |
|
01-Dec-2005 |
berghofe <none@none> |
Improved norm_proof to handle proofs containing term (type) variables with same name but different types (sorts): Offending term (type) variables are replaced by dummy (T)Frees before applying the substitution.
|
#
cd0a9904 |
|
28-Oct-2005 |
wenzelm <none@none> |
Logic.lift_all;
|
#
db589537 |
|
04-Oct-2005 |
wenzelm <none@none> |
minor tweaks for Poplog/ML;
|
#
9b308871 |
|
19-Sep-2005 |
wenzelm <none@none> |
shrink: compress terms and types; prefer member/insert over polymorphic mem/ins;
|
#
45dec154 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update;
|
#
dcefbda4 |
|
12-Sep-2005 |
haftmann <none@none> |
introduced new-style AList operations
|
#
e6334480 |
|
08-Sep-2005 |
haftmann <none@none> |
introduces some modern-style AList operations
|
#
c968ef97 |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update;
|
#
e7b1feab |
|
31-Aug-2005 |
wenzelm <none@none> |
refer to theory instead of low-level tsig;
|
#
f7c6efa7 |
|
03-Aug-2005 |
berghofe <none@none> |
- Tuned handling of oracles - Put arguments of axms_of_proof and thms_of_proof into "canonical order"
|
#
28d79992 |
|
01-Aug-2005 |
wenzelm <none@none> |
replaced atless by term_ord;
|
#
9e20a765 |
|
28-Jul-2005 |
wenzelm <none@none> |
adapted Type.typ_match; tuned;
|
#
7a547211 |
|
19-Jul-2005 |
wenzelm <none@none> |
tuned instantiate interface; Logic.incr_tvar;
|
#
53bd14d2 |
|
13-Jul-2005 |
haftmann <none@none> |
(intermediate commit)
|
#
64dca2fd |
|
22-Jun-2005 |
wenzelm <none@none> |
renamed init to init_data;
|
#
c01306d6 |
|
17-Jun-2005 |
wenzelm <none@none> |
accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
|
#
e7bf4e72 |
|
21-Apr-2005 |
berghofe <none@none> |
- Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
|
#
ecce74f9 |
|
26-Mar-2005 |
gagern <none@none> |
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
|
#
9cc62485 |
|
04-Mar-2005 |
skalberg <none@none> |
Removed practically all references to Library.foldr.
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
257fa14b |
|
09-Jul-2004 |
berghofe <none@none> |
- Expressed infer_derivs' in terms of infer_deriv - Eta-expanded function instantiate to delay evaluation (avoids inefficiencies when proof terms are switched off)
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
4ca8e7a3 |
|
31-May-2004 |
wenzelm <none@none> |
removed obsolete sort 'logic';
|
#
5102e733 |
|
21-May-2004 |
wenzelm <none@none> |
adapted tsig interface;
|
#
430b86d0 |
|
13-Dec-2002 |
berghofe <none@none> |
size_of_proof no longer includes size_of_term
|
#
1a7fa65c |
|
10-Dec-2002 |
berghofe <none@none> |
Added size_of_proof.
|
#
cbbb874b |
|
21-Oct-2002 |
berghofe <none@none> |
Removed Logic.strip_flexpairs.
|
#
e424867a |
|
07-Oct-2002 |
nipkow <none@none> |
take/drop -> splitAt
|
#
a77aeb0d |
|
27-Aug-2002 |
wenzelm <none@none> |
thms/axms_of_proof: proper handling of MinProof;
|
#
8cd6ad6b |
|
04-May-2002 |
berghofe <none@none> |
Added skeletons to speed up rewriting on proof terms.
|
#
048d77ea |
|
21-Feb-2002 |
wenzelm <none@none> |
fixed get_name_tags in order to work with hyps;
|
#
d178309d |
|
20-Feb-2002 |
berghofe <none@none> |
New function change_type for changing type assignments of theorems, axioms and oracles.
|
#
658d2e72 |
|
14-Feb-2002 |
wenzelm <none@none> |
made MLWorks happy;
|
#
ea216c1a |
|
06-Feb-2002 |
berghofe <none@none> |
Added function could_unify to speed up rewriting of proof terms.
|
#
498f55ac |
|
05-Feb-2002 |
berghofe <none@none> |
New function maxidx_of_proof.
|
#
8256d12f |
|
14-Dec-2001 |
wenzelm <none@none> |
type_env;
|
#
cadfdab8 |
|
27-Nov-2001 |
wenzelm <none@none> |
theory data: removed obsolete finish method;
|
#
b0d5bc2d |
|
24-Nov-2001 |
wenzelm <none@none> |
fixed SML/NJ error (!?);
|
#
bfef7256 |
|
24-Nov-2001 |
wenzelm <none@none> |
use merge_lists, merge_alists;
|
#
cb17348e |
|
24-Nov-2001 |
berghofe <none@none> |
Extended match_proof to handle abstractions.
|
#
e778bc2c |
|
19-Nov-2001 |
berghofe <none@none> |
- Fixed bug in shrink - Restored old behaviour of thm_proof - Eliminated reference from theory data
|
#
37c2ce11 |
|
08-Nov-2001 |
wenzelm <none@none> |
theory data: finish method;
|
#
37b6121d |
|
03-Nov-2001 |
berghofe <none@none> |
Fixed bug in function add_npvars.
|
#
31ac9557 |
|
31-Oct-2001 |
berghofe <none@none> |
Tuned function thm_proof.
|
#
f72ae51d |
|
10-Oct-2001 |
berghofe <none@none> |
Tuned several functions to improve sharing of unchanged subproofs.
|
#
47630bc4 |
|
03-Oct-2001 |
paulson <none@none> |
eta-expansion required for SML/NJ
|
#
a0f819e6 |
|
28-Sep-2001 |
berghofe <none@none> |
- Exchanged % and %%. - Fixed bug in shrink.
|
#
2fe5e2a2 |
|
31-Aug-2001 |
wenzelm <none@none> |
renamed `keep_derivs' to `proofs', and made an integer;
|
#
4d4c3d42 |
|
31-Aug-2001 |
wenzelm <none@none> |
fixed header;
|
#
70419ae6 |
|
31-Aug-2001 |
berghofe <none@none> |
New implementation of LF style proof terms.
|