#
25fb6d73 |
|
14-Mar-2020 |
wenzelm <none@none> |
more robust: proper transfer if Context.eq_thy_id;
|
#
bd91229e |
|
09-Mar-2020 |
wenzelm <none@none> |
more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);
|
#
d2806875 |
|
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;
|
#
3b657802 |
|
17-Feb-2020 |
wenzelm <none@none> |
proper sort constraints for strip_shyps, for sort relations used in minimization;
|
#
5871c403 |
|
17-Feb-2020 |
wenzelm <none@none> |
tuned;
|
#
359068c3 |
|
16-Feb-2020 |
wenzelm <none@none> |
proper sort constraints for strip_shyps, which implicitly performs type instantiation; include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer;
|
#
577c0313 |
|
28-Nov-2019 |
wenzelm <none@none> |
more structural integrity;
|
#
34ca367d |
|
08-Nov-2019 |
wenzelm <none@none> |
clarified modules;
|
#
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;
|
#
b0b3267c |
|
03-Nov-2019 |
wenzelm <none@none> |
expose derivations more thoroughly, notably for locale/class reasoning;
|
#
7547cdae |
|
03-Nov-2019 |
wenzelm <none@none> |
more robust;
|
#
51e1b2b2 |
|
03-Nov-2019 |
wenzelm <none@none> |
clarified modules;
|
#
0250919a |
|
22-Oct-2019 |
wenzelm <none@none> |
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
|
#
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;
|
#
70fb43ac |
|
19-Oct-2019 |
wenzelm <none@none> |
tuned signature;
|
#
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;
|
#
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);
|
#
a17fe1a0 |
|
10-Oct-2019 |
wenzelm <none@none> |
tuned -- more direct ML expressions;
|
#
718c279c |
|
10-Oct-2019 |
wenzelm <none@none> |
clarified modules;
|
#
821213fd |
|
10-Oct-2019 |
wenzelm <none@none> |
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
|
#
af3bddc4 |
|
09-Oct-2019 |
wenzelm <none@none> |
misc tuning and clarification;
|
#
819e925d |
|
09-Oct-2019 |
wenzelm <none@none> |
tuned -- allow slightly more expensive atomic proofs;
|
#
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;
|
#
16dcebe1 |
|
20-Aug-2019 |
wenzelm <none@none> |
unused (see 095dadc62bb5);
|
#
7d08d36e |
|
20-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
438cc573 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
d29de9af |
|
17-Aug-2019 |
wenzelm <none@none> |
discontinued peek_status: unused and not clearly defined;
|
#
f760949e |
|
17-Aug-2019 |
wenzelm <none@none> |
added ML antiquotation @{oracle_name};
|
#
f55c44db |
|
17-Aug-2019 |
wenzelm <none@none> |
more robust, notably for open_proof of unnamed derivation;
|
#
5872bc85 |
|
16-Aug-2019 |
wenzelm <none@none> |
added command 'thm_oracles';
|
#
380a3246 |
|
17-Aug-2019 |
wenzelm <none@none> |
unused;
|
#
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;
|
#
ea643178 |
|
16-Aug-2019 |
wenzelm <none@none> |
clarified derivation_name vs. raw_derivation_name;
|
#
55415b37 |
|
12-Aug-2019 |
wenzelm <none@none> |
more robust -- notably for metis, which tends to accumulate tpairs;
|
#
37bd44c0 |
|
11-Aug-2019 |
wenzelm <none@none> |
record sort constraints unconditionally: minimal performance implications;
|
#
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
#
53baa26b |
|
07-Aug-2019 |
wenzelm <none@none> |
more robust and convenient treatment of implicit context;
|
#
e3eb1d54 |
|
07-Aug-2019 |
wenzelm <none@none> |
explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;
|
#
b06d33d9 |
|
06-Aug-2019 |
wenzelm <none@none> |
backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
|
#
cd87aa9a |
|
06-Aug-2019 |
wenzelm <none@none> |
more robust and convenient treatment of implicit context;
|
#
86be8a71 |
|
05-Aug-2019 |
wenzelm <none@none> |
clarified modules: more direct data implementation;
|
#
1bc0d395 |
|
03-Aug-2019 |
wenzelm <none@none> |
more efficient data structure;
|
#
2026a703 |
|
03-Aug-2019 |
wenzelm <none@none> |
guard constraints by record_proofs=1, until performance implications have become more clear;
|
#
bc758047 |
|
03-Aug-2019 |
wenzelm <none@none> |
more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;
|
#
be3a5564 |
|
03-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
ba0f95af |
|
03-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
c735136b |
|
02-Aug-2019 |
wenzelm <none@none> |
maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms; tuned;
|
#
e91e3ab4 |
|
02-Aug-2019 |
wenzelm <none@none> |
more direct proofs for type classes; misc tuning and cleanup;
|
#
f4e209bb |
|
02-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
aede6033 |
|
02-Aug-2019 |
wenzelm <none@none> |
clarified modules: inference kernel maintains sort algebra within the logic;
|
#
c24dd438 |
|
01-Aug-2019 |
wenzelm <none@none> |
clarified module structure;
|
#
4458ff41 |
|
01-Aug-2019 |
wenzelm <none@none> |
simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);
|
#
82dd600e |
|
24-Jul-2019 |
wenzelm <none@none> |
clarified modules;
|
#
6ce0a4e1 |
|
22-Jul-2019 |
wenzelm <none@none> |
proof terms are always constructed sequentially; discontinued unused Proofterm.Promise -- too complex;
|
#
04b63c2e |
|
03-Jun-2019 |
wenzelm <none@none> |
more structural integrity;
|
#
658cb625 |
|
03-Jun-2019 |
wenzelm <none@none> |
clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;
|
#
c93a1841 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned signature;
|
#
4bbaf8f5 |
|
13-Apr-2019 |
wenzelm <none@none> |
more ctyp operations;
|
#
14d23f61 |
|
13-Apr-2019 |
wenzelm <none@none> |
prefer exception TYPE, e.g. when used within conversion;
|
#
dead1326 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned signature -- more ctyp operations;
|
#
916cec10 |
|
01-Oct-2018 |
wenzelm <none@none> |
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
|
#
083b2ecc |
|
27-Jul-2018 |
wenzelm <none@none> |
proper maxidx: if x does not occur in A, its maxidx could get lost;
|
#
52d90ad5 |
|
27-Jul-2018 |
wenzelm <none@none> |
tuned;
|
#
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap; tuned comments;
|
#
d3b9e5cc |
|
21-Feb-2018 |
wenzelm <none@none> |
more operations for ctyp, cterm;
|
#
ba9cb2ae |
|
18-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
#
a2be8a0d |
|
02-Jan-2018 |
haftmann <none@none> |
repaired whitespace accident from 2505cabfc515
|
#
8da77906 |
|
01-Jan-2018 |
haftmann <none@none> |
proper namespace for evaluators --HG-- extra : rebase_source : cbf47061c33ac1e0a221ab6513662ecd3e78c71d
|
#
f30be3c8 |
|
22-Jun-2017 |
wenzelm <none@none> |
consolidate proofs more simultaneously;
|
#
151b7ea2 |
|
10-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
#
dd849a8b |
|
03-Feb-2017 |
wenzelm <none@none> |
proper background certificate from make_context, which can be a super-theory of the direct join (amending d07464875dd4);
|
#
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;
|
#
9752bbd7 |
|
15-Dec-2016 |
wenzelm <none@none> |
tuned;
|
#
a0d0cb73 |
|
15-Dec-2016 |
wenzelm <none@none> |
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
|
#
e33b0cb4 |
|
14-Dec-2016 |
wenzelm <none@none> |
more careful derivation_closed / close_derivation;
|
#
80b2c3e6 |
|
12-Sep-2016 |
wenzelm <none@none> |
tuned;
|
#
15568a29 |
|
05-Aug-2016 |
wenzelm <none@none> |
tuned whitespace;
|
#
89c7cc9e |
|
30-Aug-2015 |
wenzelm <none@none> |
tuned;
|
#
90a96b58 |
|
30-Aug-2015 |
wenzelm <none@none> |
clarified exceptions; tuned signature;
|
#
fa60c9ec |
|
30-Aug-2015 |
wenzelm <none@none> |
clarified exceptions; more careful treatment of missing context;
|
#
ff1277af |
|
29-Aug-2015 |
wenzelm <none@none> |
trim context for persistent storage;
|
#
710095ed |
|
30-Aug-2015 |
wenzelm <none@none> |
clarified exceptions;
|
#
0affb1b3 |
|
28-Aug-2015 |
wenzelm <none@none> |
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
|
#
aac03669 |
|
28-Aug-2015 |
wenzelm <none@none> |
more abstract theory certificate, which is not necessarily the full theory;
|
#
ab684e0d |
|
28-Aug-2015 |
wenzelm <none@none> |
tuned signature;
|
#
a4dd316d |
|
28-Aug-2015 |
wenzelm <none@none> |
tuned signature;
|
#
db363f3c |
|
16-Aug-2015 |
wenzelm <none@none> |
produce certified vars without access to theory_of_thm, and without context;
|
#
c326e8e1 |
|
16-Aug-2015 |
wenzelm <none@none> |
produce certified vars without access to theory_of_thm, and without context;
|
#
bc3d393f |
|
16-Aug-2015 |
wenzelm <none@none> |
added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
|
#
02f6d501 |
|
16-Aug-2015 |
wenzelm <none@none> |
prefer theory_id operations; tuned signature;
|
#
5e727913 |
|
15-Aug-2015 |
wenzelm <none@none> |
obsolete;
|
#
0226e5de |
|
28-Jul-2015 |
wenzelm <none@none> |
more direct access to atomic cterms;
|
#
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
#
48e2d74a |
|
03-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
d0279931 |
|
30-May-2015 |
wenzelm <none@none> |
more explicit context;
|
#
6e829806 |
|
08-Apr-2015 |
wenzelm <none@none> |
explicitly checked alpha conversion -- actual renaming happens outside kernel;
|
#
94e11df0 |
|
03-Apr-2015 |
wenzelm <none@none> |
more uniform "verbose" option to print name space;
|
#
70c854b1 |
|
31-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
54f4e638 |
|
23-Mar-2015 |
wenzelm <none@none> |
local fixes may depend on goal params;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
61ae4b88 |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
39c46b89 |
|
04-Mar-2015 |
wenzelm <none@none> |
removed unused; tuned comments;
|
#
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
16b4f761 |
|
08-Nov-2014 |
wenzelm <none@none> |
optional proof context for unify operations, for the sake of proper local options;
|
#
49b7e0a1 |
|
08-Nov-2014 |
wenzelm <none@none> |
proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
|
#
ab11590d |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
6f587f58 |
|
11-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
98c7fb02 |
|
10-Mar-2014 |
wenzelm <none@none> |
abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
|
#
d7704814 |
|
30-Jul-2013 |
wenzelm <none@none> |
tuned;
|
#
42e9b2b9 |
|
30-Jul-2013 |
wenzelm <none@none> |
type theory is purely value-oriented;
|
#
48675c42 |
|
19-Jul-2013 |
wenzelm <none@none> |
turned pattern unify flag into configuration option (global only);
|
#
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;
|
#
1b1fb1e5 |
|
29-May-2013 |
wenzelm <none@none> |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
#
7ec0a377 |
|
29-May-2013 |
wenzelm <none@none> |
unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
|
#
e712bb09 |
|
24-May-2013 |
wenzelm <none@none> |
tuned signature;
|
#
97779172 |
|
03-Apr-2013 |
wenzelm <none@none> |
updated comment to 46b90bbc370d;
|
#
d6c62ebd |
|
30-Nov-2012 |
wenzelm <none@none> |
print formal entities with markup;
|
#
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;
|
#
b7d9af80 |
|
30-Aug-2012 |
wenzelm <none@none> |
proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
|
#
78ad7f75 |
|
15-Jul-2012 |
wenzelm <none@none> |
prefer canonical fold_rev;
|
#
551b966c |
|
18-Mar-2012 |
wenzelm <none@none> |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
|
#
0d27b506 |
|
15-Feb-2012 |
wenzelm <none@none> |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
#
18cde334 |
|
14-Feb-2012 |
wenzelm <none@none> |
tuned signature;
|
#
c3a756c9 |
|
25-Jan-2012 |
wenzelm <none@none> |
removed obscure/outdated material;
|
#
ca981f61 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
#
ab54c3b1 |
|
14-Jan-2012 |
wenzelm <none@none> |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
#
6fe01930 |
|
10-Nov-2011 |
wenzelm <none@none> |
discontinued unused Thm.compress (again);
|
#
b811b2f5 |
|
03-Nov-2011 |
wenzelm <none@none> |
tuned signature;
|
#
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;
|
#
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;
|
#
fc107ff5 |
|
17-Aug-2011 |
wenzelm <none@none> |
more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
|
#
fd55586e |
|
09-Aug-2011 |
berghofe <none@none> |
rename_bvs now avoids introducing name clashes between schematic variables
|
#
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;
|
#
390ebc4a |
|
08-Jun-2011 |
wenzelm <none@none> |
more robust exception pattern General.Subscript;
|
#
fa8535c2 |
|
20-Apr-2011 |
wenzelm <none@none> |
added Theory.nodes_of convenience;
|
#
13a7cd41 |
|
17-Apr-2011 |
wenzelm <none@none> |
report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
|
#
87db399e |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
e7602b11 |
|
16-Apr-2011 |
wenzelm <none@none> |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
#
f005184f |
|
03-Feb-2011 |
wenzelm <none@none> |
thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
|
#
17eb06fd |
|
03-Feb-2011 |
wenzelm <none@none> |
tuned comments;
|
#
8dc52649 |
|
28-Oct-2010 |
wenzelm <none@none> |
type attribute is derived concept outside the kernel;
|
#
5743c6b5 |
|
25-Oct-2010 |
wenzelm <none@none> |
recovered some odd two-dimensional layout;
|
#
86bc1118 |
|
24-Sep-2010 |
wenzelm <none@none> |
modernized structure Ord_List;
|
#
049938fe |
|
25-Aug-2010 |
wenzelm <none@none> |
structure Thm: less pervasive names;
|
#
6e4dcf7a |
|
03-Jun-2010 |
wenzelm <none@none> |
eliminated ML structure alias;
|
#
d8a8dc0a |
|
02-Jun-2010 |
wenzelm <none@none> |
always unconstrain thm proofs;
|
#
770826b9 |
|
19-May-2010 |
haftmann <none@none> |
dropped legacy_unconstrainT
|
#
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;
|
#
61f7b2df |
|
09-May-2010 |
wenzelm <none@none> |
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
|
#
86b56177 |
|
09-May-2010 |
wenzelm <none@none> |
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
|
#
08789841 |
|
09-May-2010 |
wenzelm <none@none> |
just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
|
#
97b990a6 |
|
08-May-2010 |
wenzelm <none@none> |
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
|
#
e3aceea5 |
|
08-May-2010 |
wenzelm <none@none> |
tuned signature;
|
#
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;
|
#
260d4e35 |
|
04-May-2010 |
wenzelm <none@none> |
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
|
#
9aff7f3d |
|
03-May-2010 |
wenzelm <none@none> |
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
#
53efcab8 |
|
03-May-2010 |
wenzelm <none@none> |
minor tuning of Thm.strip_shyps -- no longer pervasive;
|
#
62097ce5 |
|
03-May-2010 |
wenzelm <none@none> |
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
|
#
0c16feb6 |
|
25-Apr-2010 |
wenzelm <none@none> |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;
|
#
b6b6d7c8 |
|
27-Mar-2010 |
wenzelm <none@none> |
added Term.fold_atyps_sorts convenience;
|
#
92bdacd4 |
|
21-Mar-2010 |
wenzelm <none@none> |
Logic.mk_of_sort convenience;
|
#
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
|
#
7bd1a61e |
|
21-Nov-2009 |
wenzelm <none@none> |
explicitly mark some legacy freeze operations;
|
#
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;
|
#
105f07d1 |
|
15-Nov-2009 |
wenzelm <none@none> |
tuned;
|
#
71833c27 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Theory_Data; tuned;
|
#
a00d61a9 |
|
25-Oct-2009 |
wenzelm <none@none> |
make SML/NJ happy;
|
#
aa0f9eb7 |
|
24-Oct-2009 |
wenzelm <none@none> |
maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
|
#
713fc456 |
|
24-Oct-2009 |
wenzelm <none@none> |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
#
4b3225d2 |
|
24-Oct-2009 |
wenzelm <none@none> |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
#
8eb709ab |
|
20-Oct-2009 |
haftmann <none@none> |
curried inter as canonical list operation (beware of argument order)
|
#
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;
|
#
2f14c9ed |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated redundant bindings;
|
#
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;
|
#
d17c3b91 |
|
27-Sep-2009 |
wenzelm <none@none> |
tuned internal source structure;
|
#
50bc5fef |
|
16-Sep-2009 |
wenzelm <none@none> |
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
|
#
3dbff3fc |
|
26-Jul-2009 |
wenzelm <none@none> |
lambda/cabs/all: named variants;
|
#
7f802f38 |
|
21-Jul-2009 |
wenzelm <none@none> |
simultaneous join_proofs; removed obsolete promises_of;
|
#
04f604b2 |
|
21-Jul-2009 |
wenzelm <none@none> |
prefer simultaneous join -- for improved scheduling;
|
#
eb7346ef |
|
19-Jul-2009 |
wenzelm <none@none> |
support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies); export promises_of; removed obsolete pending_groups; tuned;
|
#
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;
|
#
196435a0 |
|
09-Jul-2009 |
wenzelm <none@none> |
renamed structure TermSubst to Term_Subst;
|
#
bad90cf2 |
|
06-Jul-2009 |
wenzelm <none@none> |
clarified strip_shyps: proper type witnesses for present sorts; moved fold_terms to thm.ML;
|
#
d62b04dd |
|
06-Jul-2009 |
wenzelm <none@none> |
structure Thm: less pervasive names;
|
#
5e95080e |
|
06-Jul-2009 |
wenzelm <none@none> |
clarified Thm.of_class/of_sort/class_triv;
|
#
2bcff546 |
|
06-Jul-2009 |
wenzelm <none@none> |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
#
43a80d4a |
|
02-Jul-2009 |
wenzelm <none@none> |
strip_shyps: remove top sort, which is logically insignificant;
|
#
968dc814 |
|
02-Jul-2009 |
wenzelm <none@none> |
added pro-forma proof constructor Inclass;
|
#
420becfd |
|
25-Mar-2009 |
wenzelm <none@none> |
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete); more explicit oracle_proof;
|
#
e6511425 |
|
24-Mar-2009 |
wenzelm <none@none> |
status_of: need to include local promises as well!
|
#
6a79c913 |
|
24-Mar-2009 |
wenzelm <none@none> |
display derivation status of thms;
|
#
949efbab |
|
16-Mar-2009 |
wenzelm <none@none> |
eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly; tuned;
|
#
33abb9e3 |
|
16-Mar-2009 |
wenzelm <none@none> |
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
|
#
3c4dea06 |
|
12-Mar-2009 |
wenzelm <none@none> |
renamed NameSpace.bind to NameSpace.define;
|
#
3a17a488 |
|
07-Mar-2009 |
wenzelm <none@none> |
moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;
|
#
2c10cf68 |
|
05-Mar-2009 |
wenzelm <none@none> |
Thm.add_oracle interface: replaced old bstring by binding;
|
#
d9512627 |
|
26-Jan-2009 |
wenzelm <none@none> |
thm_proof: replaced lazy by composed futures;
|
#
11ff1eb6 |
|
10-Jan-2009 |
wenzelm <none@none> |
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
|
#
83e9770e |
|
10-Jan-2009 |
wenzelm <none@none> |
added pending_groups -- accumulates task groups of local derivations only;
|
#
5ff9b5cb |
|
01-Jan-2009 |
wenzelm <none@none> |
avoid polymorphic equality;
|
#
e5a0650c |
|
31-Dec-2008 |
wenzelm <none@none> |
use regular Term.add_XXX etc.;
|
#
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
|
#
9dcb68ba |
|
05-Dec-2008 |
wenzelm <none@none> |
renamed force_proof to join_proof;
|
#
b36ff989 |
|
05-Dec-2008 |
wenzelm <none@none> |
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises); name_thm: actually maintain max_promise/open_promises here (!), reduce open_promises as far as possible; tuned;
|
#
4c569229 |
|
05-Dec-2008 |
haftmann <none@none> |
dropped NameSpace.declare_base
|
#
b7f866d2 |
|
04-Dec-2008 |
wenzelm <none@none> |
future proofs: pass actual futures to facilitate composite computations; removed join_futures -- superceded by higher-level PureThy.force_proofs;
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
cf7bb7d8 |
|
23-Nov-2008 |
wenzelm <none@none> |
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
|
#
a6df7fbd |
|
18-Nov-2008 |
wenzelm <none@none> |
fulfill_proof/thm_proof: commuted lazyness; join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);
|
#
8cc4cd7a |
|
18-Nov-2008 |
wenzelm <none@none> |
added force_proofs; join_futures: no errors here;
|
#
bfab2724 |
|
17-Nov-2008 |
wenzelm <none@none> |
tuned promise/fullfill;
|
#
6b548cc7 |
|
16-Nov-2008 |
wenzelm <none@none> |
put_name/thm_proof: promises are filled with fulfilled proofs; tuned;
|
#
8e16d38f |
|
16-Nov-2008 |
wenzelm <none@none> |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
#
88b6d409 |
|
15-Nov-2008 |
wenzelm <none@none> |
refined notion of derivation, consiting of promises and proof_body; removed oracle_of (would require detailed check wrt. promises); proof_of returns proof_body;
|
#
e5d337e2 |
|
23-Oct-2008 |
wenzelm <none@none> |
renamed get_axiom_i to axiom, removed obsolete get_axiom; reduced pervasive names;
|
#
017f28aa |
|
21-Oct-2008 |
wenzelm <none@none> |
join results in isolation;
|
#
b8454803 |
|
16-Oct-2008 |
wenzelm <none@none> |
added weaken_sorts; strip_shyps: minimal list of minimized extra sorts; tuned;
|
#
b2cc1b1e |
|
30-Sep-2008 |
wenzelm <none@none> |
renamed promise to future, tuned related interfaces;
|
#
fd43830e |
|
30-Sep-2008 |
wenzelm <none@none> |
more precise join_futures, improved termination;
|
#
a92c90c9 |
|
30-Sep-2008 |
wenzelm <none@none> |
export explicit joint_futures, removed Theory.at_end hook; renamed Future.fork_irrelevant to Future.fork_background;
|
#
30653b1b |
|
27-Sep-2008 |
wenzelm <none@none> |
join earlier promises first;
|
#
3fac88cf |
|
27-Sep-2008 |
wenzelm <none@none> |
promise_result: enforce strictly sequential dependencies, via serial numbers;
|
#
c1837a6f |
|
27-Sep-2008 |
wenzelm <none@none> |
Future.release_results;
|
#
c96c4394 |
|
27-Sep-2008 |
wenzelm <none@none> |
promise: include check into future body, i.e. joined results are always valid; pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory; simplified rep_deriv;
|
#
019c4222 |
|
25-Sep-2008 |
wenzelm <none@none> |
simplified promise; fulfill is internal only; more robust join_futures;
|
#
947c8d5e |
|
25-Sep-2008 |
wenzelm <none@none> |
abtract types: plain datatype with opaque signature matching; promise: join pending futures at end of theory;
|
#
4ff1faf4 |
|
25-Sep-2008 |
wenzelm <none@none> |
explicit type OrdList.T;
|
#
28312e9d |
|
23-Sep-2008 |
wenzelm <none@none> |
added dest_deriv, removed external type deriv; misc tuning of internal deriv; more substantial promise/fulfill; promise_ord: reverse order on serial numbers; removed unused is_named; get_name: unfinished proof term;
|
#
9a1849b0 |
|
22-Sep-2008 |
wenzelm <none@none> |
type thm: fully internal derivation, no longer exported; incorporate former deriv.ML as internal abstract type; added rudimentary promise interface; tuned; added is_named (does not require finished derivation);
|
#
9f686374 |
|
18-Sep-2008 |
wenzelm <none@none> |
simplified oracle interface;
|
#
a269eae7 |
|
18-Sep-2008 |
wenzelm <none@none> |
added deriv.ML: Abstract derivations based on raw proof terms.
|
#
d0b84733 |
|
27-Aug-2008 |
wenzelm <none@none> |
type Properties.T;
|
#
26bc0582 |
|
23-Jun-2008 |
wenzelm <none@none> |
Logic.all/mk_equals/mk_implies; Term.all;
|
#
70a4fc69 |
|
18-May-2008 |
wenzelm <none@none> |
moved global pretty/string_of functions from Sign to Syntax;
|
#
d9b4209c |
|
07-May-2008 |
berghofe <none@none> |
eq_assumption now uses aeconv instead of aconv.
|
#
4fd826a1 |
|
15-Apr-2008 |
wenzelm <none@none> |
Theory.eq_thy;
|
#
155224ff |
|
13-Apr-2008 |
wenzelm <none@none> |
simplified handling of sorts, removed unnecessary universal witness; Envir.insert_sorts;
|
#
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;
|
#
d5272fc3 |
|
21-Jan-2008 |
berghofe <none@none> |
Removed Logic.auto_rename.
|
#
0e30ca26 |
|
04-Oct-2007 |
wenzelm <none@none> |
replaced literal 'a by Name.aT;
|
#
9c57c64f |
|
17-Aug-2007 |
wenzelm <none@none> |
compress: proper check_thy;
|
#
ae875ba0 |
|
03-Aug-2007 |
wenzelm <none@none> |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref; thread-safeness: when creating certified items, perform Theory.check_thy *last*;
|
#
7a97993d |
|
11-Jul-2007 |
berghofe <none@none> |
Added function norm_proof for normalizing the proof term corresponding to a theorem.
|
#
792d3082 |
|
08-Jul-2007 |
wenzelm <none@none> |
thm tag: Markup.property list;
|
#
2ad041f9 |
|
05-Jul-2007 |
wenzelm <none@none> |
added type conv; merge_thys: removed dead exception handlers; tuned;
|
#
737f6ede |
|
24-Jun-2007 |
wenzelm <none@none> |
added eta_long_conversion;
|
#
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;
|
#
2bfe4ad1 |
|
09-May-2007 |
wenzelm <none@none> |
added dest_fun/fun2/arg1; removed dest_binop; renamed cterm_(fo_)match to (fo_)match; renamed cterm_incr_indexes to incr_indexes_cterm;
|
#
4d68fcc4 |
|
14-Apr-2007 |
wenzelm <none@none> |
removed obsolete read_ctyp, read_def_cterm; moved read_def_cterms, read_cterm to more_thm.ML; avoid rep_theory;
|
#
e7f94b57 |
|
04-Apr-2007 |
wenzelm <none@none> |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
#
153c14aa |
|
03-Apr-2007 |
wenzelm <none@none> |
improved exception CTERM; added instantiate_cterm; removed obsolete sign_of_thm;
|
#
6fb626be |
|
03-Apr-2007 |
wenzelm <none@none> |
avoid clash with Alice keywords;
|
#
a5231007 |
|
26-Feb-2007 |
wenzelm <none@none> |
moved some non-kernel material to more_thm.ML;
|
#
41fa38b5 |
|
04-Feb-2007 |
wenzelm <none@none> |
old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;
|
#
2b590625 |
|
02-Jan-2007 |
wenzelm <none@none> |
Term.lambda: abstract over arbitrary closed terms;
|
#
110e4b19 |
|
12-Dec-2006 |
wenzelm <none@none> |
tuned error messages;
|
#
b5dac97b |
|
04-Dec-2006 |
wenzelm <none@none> |
thm/prf: separate official name vs. additional tags;
|
#
b7957923 |
|
28-Nov-2006 |
wenzelm <none@none> |
simplified Logic.count_prems;
|
#
05d1b149 |
|
21-Nov-2006 |
wenzelm <none@none> |
moved theorem kinds from PureThy to Thm;
|
#
a8c1bbaa |
|
05-Nov-2006 |
wenzelm <none@none> |
removed obsolete first_duplicate;
|
#
592de03a |
|
31-Oct-2006 |
haftmann <none@none> |
fixed type signature of Type.varify
|
#
ea4e499c |
|
11-Oct-2006 |
haftmann <none@none> |
abandoned findrep
|
#
ab96bc46 |
|
06-Oct-2006 |
wenzelm <none@none> |
added def_name_optional;
|
#
ded194cb |
|
01-Oct-2006 |
wenzelm <none@none> |
cterm_match: avoid recalculation of maxidx;
|
#
fcdcf5df |
|
21-Sep-2006 |
wenzelm <none@none> |
added dest_binop;
|
#
15a27c5d |
|
18-Sep-2006 |
wenzelm <none@none> |
added dest_arg, i.e. a tuned version of #2 o dest_comb;
|
#
e69dd782 |
|
15-Sep-2006 |
wenzelm <none@none> |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
#
b79df5df |
|
15-Sep-2006 |
wenzelm <none@none> |
instantiate: omit has_duplicates check, which is irrelevant for soundness;
|
#
783c0e30 |
|
11-Sep-2006 |
wenzelm <none@none> |
ctyp: maintain maxidx; cterm_match: tight maxidx for substitution; instantiate: determine maxidx from insts -- major performance improvement; moved term subst functions to TermSubst; tuned;
|
#
08b261b8 |
|
08-Aug-2006 |
haftmann <none@none> |
abandoned equal_list in favor for eq_list
|
#
b07a7724 |
|
03-Aug-2006 |
wenzelm <none@none> |
tuned;
|
#
66cc9615 |
|
02-Aug-2006 |
wenzelm <none@none> |
normalized Proof.context/method type aliases;
|
#
7e813229 |
|
30-Jul-2006 |
wenzelm <none@none> |
adjust_maxidx: pass explicit lower bound; tuned interfaces;
|
#
35141c3c |
|
10-Jul-2006 |
wenzelm <none@none> |
replaced Term.variant(list) by Name.variant(_list);
|
#
ccff77d3 |
|
07-Jul-2006 |
wenzelm <none@none> |
tuned exception handling;
|
#
86594932 |
|
04-Jul-2006 |
wenzelm <none@none> |
varifyT: no longer pervasive;
|
#
ef1320d5 |
|
17-Jun-2006 |
wenzelm <none@none> |
added generalize rule; added maxidx_thm;
|
#
080989ef |
|
13-Jun-2006 |
wenzelm <none@none> |
added hyps_of; tuned;
|
#
66ebcc39 |
|
12-Jun-2006 |
wenzelm <none@none> |
tuned Seq/Envir/Unify interfaces;
|
#
f14cb302 |
|
01-May-2006 |
wenzelm <none@none> |
class_triv: Sign.certify_class;
|
#
a6ee3e1d |
|
29-Apr-2006 |
wenzelm <none@none> |
added unconstrainT;
|
#
e165241c |
|
26-Apr-2006 |
wenzelm <none@none> |
curried Seq.cons;
|
#
d9467697 |
|
12-Apr-2006 |
wenzelm <none@none> |
added maxidx_of;
|
#
80d65d44 |
|
20-Mar-2006 |
wenzelm <none@none> |
avoid polymorphic equality;
|
#
4025fa48 |
|
09-Mar-2006 |
mengj <none@none> |
Shortened the exception messages from assume.
|
#
6bee66ba |
|
11-Feb-2006 |
wenzelm <none@none> |
tuned;
|
#
e67f8f27 |
|
07-Feb-2006 |
wenzelm <none@none> |
removed obsolete sign_of_cterm; adapted Sign.certify_term;
|
#
30cc86b6 |
|
06-Feb-2006 |
wenzelm <none@none> |
union_tpairs: Library.merge; Envir.(beta_)eta_contract; tuned;
|
#
85d37bc2 |
|
21-Jan-2006 |
wenzelm <none@none> |
simplified type attribute; added rule/declaration_attribute (from drule.ML); added theory/proof_attributes; removed apply(s)_attributes;
|
#
be6642c8 |
|
23-Dec-2005 |
wenzelm <none@none> |
turned bicompose_no_flatten into compose_no_flatten, without elimination;
|
#
7a3ac59b |
|
21-Dec-2005 |
wenzelm <none@none> |
added bicompose_no_flatten, which refrains from changing the shape of the new subgoals;
|
#
d3b022c7 |
|
16-Dec-2005 |
haftmann <none@none> |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
#
bc119b67 |
|
16-Nov-2005 |
wenzelm <none@none> |
tuned Pattern.match/unify;
|
#
1a9d0572 |
|
10-Nov-2005 |
wenzelm <none@none> |
renamed Thm.cgoal_of to Thm.cprem_of;
|
#
378a8da5 |
|
09-Nov-2005 |
wenzelm <none@none> |
Thm.varifyT': natural argument order;
|
#
dcbefbcf |
|
28-Oct-2005 |
wenzelm <none@none> |
added cgoal_of; simplified lift_rule: take goal cterm instead of goal state thm, use Logic.lift_abs/all;
|
#
828ee4f8 |
|
14-Oct-2005 |
wenzelm <none@none> |
tuned comment;
|
#
bbf10dcd |
|
28-Sep-2005 |
wenzelm <none@none> |
abstract_rule: tuned exception msgs;
|
#
45dec154 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update;
|
#
fe2499cf |
|
13-Sep-2005 |
wenzelm <none@none> |
added simple_fact; generalized no_attributes;
|
#
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;
|
#
2085d1ed |
|
29-Aug-2005 |
wenzelm <none@none> |
use AList operations;
|
#
0838c364 |
|
01-Aug-2005 |
wenzelm <none@none> |
Compress.term;
|
#
379fa3ff |
|
28-Jul-2005 |
wenzelm <none@none> |
added weaken, adjust_maxidx_thm;
|
#
0b76e876 |
|
19-Jul-2005 |
wenzelm <none@none> |
tuned instantiate (avoid subst_atomic, subst_atomic_types); Logic.incr_tvar;
|
#
fe57ea23 |
|
14-Jul-2005 |
wenzelm <none@none> |
invoke_oracle: do not keep theory value, but theory_ref;
|
#
c5b2cea9 |
|
06-Jul-2005 |
wenzelm <none@none> |
added full_prop_of: includes tpairs;
|
#
32f01479 |
|
06-Jul-2005 |
wenzelm <none@none> |
tuned maxidx;
|
#
7520f7c6 |
|
04-Jul-2005 |
wenzelm <none@none> |
dest_ctyp: raise exception for non-constructor; dest_comb: replaced expensive fastype_of by Term.argument_type; dest_abs: replaced expensive variant_abs by Term.dest_abs; hyps: fast_term_ord;
|
#
a3d8b165 |
|
01-Jul-2005 |
wenzelm <none@none> |
ctyp: added 'sorts' field; may_insert_typ/term/env_sorts: observe Sign.all_sorts_nonempty; may_insert_env_sorts: insert sorts of type subst only; instantiate: insert sorts of insts; tuned;
|
#
b48c7186 |
|
29-Jun-2005 |
wenzelm <none@none> |
more efficient treatment of shyps and hyps (use ordered lists); added 'sorts' field to cterm; removed obsolete fix_shyps; moved implies_intr_hyps to drule.ML;
|
#
8c6c7807 |
|
17-Jun-2005 |
wenzelm <none@none> |
accomodate identification of type Sign.sg and theory;
|
#
45cc01c5 |
|
08-Jun-2005 |
wenzelm <none@none> |
axioms: NameSpace.table;
|
#
78a97290 |
|
05-Jun-2005 |
wenzelm <none@none> |
Type.freeze;
|
#
dcb54a9b |
|
31-May-2005 |
wenzelm <none@none> |
added eq_thms;
|
#
0ed1a6c3 |
|
22-May-2005 |
wenzelm <none@none> |
tuned terms_of_tpairs;
|
#
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.
|
#
ffbc1314 |
|
07-Apr-2005 |
wenzelm <none@none> |
added get_axiom_i, invoke_oracle_i;
|
#
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.
|
#
f993d1a6 |
|
23-Jan-2005 |
paulson <none@none> |
thin_tac now works on P==>Q
|
#
64cb53f4 |
|
26-Oct-2004 |
berghofe <none@none> |
Changed function cabs to also allow abstraction over Vars.
|
#
daad2b78 |
|
29-Jul-2004 |
berghofe <none@none> |
- optimized nodup_vars check in capply - new function dest_ctyp
|
#
40c81668 |
|
29-May-2004 |
wenzelm <none@none> |
improved output; refer to Pretty.pp;
|
#
30c727cd |
|
21-May-2004 |
wenzelm <none@none> |
adapted names of some sort ops;
|
#
3e36550b |
|
21-Oct-2002 |
berghofe <none@none> |
Changed handling of flex-flex constraints: now stored in separate tpairs field of theorem record.
|
#
7fffca59 |
|
10-Oct-2002 |
nipkow <none@none> |
added failure trace information to pattern unification
|
#
e424867a |
|
07-Oct-2002 |
nipkow <none@none> |
take/drop -> splitAt
|
#
7bc53650 |
|
27-Aug-2002 |
wenzelm <none@none> |
added proof_of;
|
#
ccd056b0 |
|
28-Feb-2002 |
wenzelm <none@none> |
moved match_bvs, match_bvars, renAbs to term.ML;
|
#
048d77ea |
|
21-Feb-2002 |
wenzelm <none@none> |
fixed get_name_tags in order to work with hyps;
|
#
913b178f |
|
17-Jan-2002 |
wenzelm <none@none> |
added prop_of: thm -> term (at last!);
|
#
7354e4ff |
|
14-Dec-2001 |
wenzelm <none@none> |
varifyT' returns newly introduces variables;
|
#
2fad0b14 |
|
04-Oct-2001 |
wenzelm <none@none> |
major_prem_of: Logic.strip_assums_concl;
|
#
d5d7e2cc |
|
28-Sep-2001 |
berghofe <none@none> |
Exchanged % and %%.
|
#
22fad3bb |
|
13-Sep-2001 |
berghofe <none@none> |
Fixed proof term bug in permute_prems.
|
#
8eeaef09 |
|
31-Aug-2001 |
berghofe <none@none> |
Replaced old derivations by proof terms.
|
#
599ed539 |
|
03-Jan-2001 |
wenzelm <none@none> |
Thm: dest_comb, dest_abs, capply, cabs no longer global;
|
#
188e258b |
|
17-Nov-2000 |
wenzelm <none@none> |
Envir.beta_norm;
|
#
26244e71 |
|
07-Nov-2000 |
berghofe <none@none> |
- Moved rewriting functions to meta_simplifier.ML - dest_abs now also takes an optional variable name as an argument - beta_conversion takes additional flag as an argument. Fully reduces the term if set to true Some tuning: - tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive, transitive, beta_conversion, abstract_rule - combination: chktypes derives types of f and t from type of == instead of using fastype_of New primitives: - eta_conversion - incr_indexes: increment indexes in theorems - cterm_incr_indexes: increment indexes in cterms - cterm_match, cterm_first_order_match - rename_boundvars
|
#
97c05a1d |
|
27-Oct-2000 |
wenzelm <none@none> |
back to 1.167, due to Emacs/CVS casualty!!;
|
#
e086559b |
|
27-Oct-2000 |
wenzelm <none@none> |
*** empty log message ***
|
#
e7539d2c |
|
07-Sep-2000 |
nipkow <none@none> |
Added meaningful output to cong-error msg.
|
#
53155ca0 |
|
29-Aug-2000 |
nipkow <none@none> |
*** empty log message ***
|
#
6f0466ab |
|
16-Aug-2000 |
nipkow <none@none> |
Fixed completeness bug in simplifier: congruence rules could preclude rewrites of the partially applied constant.
|
#
c9143b96 |
|
02-Aug-2000 |
wenzelm <none@none> |
derivations: maintain oracle flag;
|
#
e9dfc7ea |
|
29-Jul-2000 |
wenzelm <none@none> |
added sign_of_cterm;
|
#
62bd508f |
|
03-Jun-2000 |
wenzelm <none@none> |
fixed Thm.eq_thm: use Sign.joinable;
|
#
3e756f28 |
|
10-May-2000 |
wenzelm <none@none> |
dest_mss: sort procs wrt. names;
|
#
cb6641bd |
|
08-May-2000 |
wenzelm <none@none> |
tuned msg;
|
#
7ee16252 |
|
30-Mar-2000 |
wenzelm <none@none> |
read_def_cterms: use Sign.read_def_terms;
|
#
4c8f4e82 |
|
10-Mar-2000 |
berghofe <none@none> |
Envir now uses Vartab instead of association lists.
|
#
71910775 |
|
27-Feb-2000 |
wenzelm <none@none> |
added major_prem_of;
|
#
8b6ef9e5 |
|
24-Feb-2000 |
wenzelm <none@none> |
tuned;
|
#
55f203c4 |
|
24-Feb-2000 |
wenzelm <none@none> |
capply, cabs: Sign.nodup_vars;
|
#
92b37e79 |
|
17-Jan-2000 |
paulson <none@none> |
Thm.instantiate no longer normalizes, but Drule.instantiate does
|
#
c55fc51a |
|
16-Dec-1999 |
paulson <none@none> |
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect nested parameters such as !!y. Goal "!!x. x = a ==> (!!y. y ~= a ==> False)"; by (rotate_tac 1 1); be notE 1; ba 1; qed "foo"; val FalseI = standard (True_not_False RS (standard (refl RS foo)));
|
#
91967eda |
|
22-Oct-1999 |
wenzelm <none@none> |
debug_simp;
|
#
71f569e0 |
|
29-Sep-1999 |
wenzelm <none@none> |
removed implies_intr_shyps; removed force_strip_shyps (at last!); strip_shyps: proper witness_sorts; fix_shyps: tuned for all_sorts_nonempty;
|
#
da8572ec |
|
09-Sep-1999 |
wenzelm <none@none> |
added no_prems;
|
#
6e19ff0b |
|
08-Sep-1999 |
wenzelm <none@none> |
removed obsolete comment;
|
#
0df2cf4f |
|
23-Aug-1999 |
nipkow <none@none> |
Now rewrite rules with flexible heads are allowed.
|
#
bca9bf62 |
|
23-Aug-1999 |
nipkow <none@none> |
Corrected two busg in the simplifier.
|
#
8bf20d8c |
|
18-Aug-1999 |
wenzelm <none@none> |
(*no fix_shyps*);
|
#
c9d4de4b |
|
18-Aug-1999 |
paulson <none@none> |
new primitive rule permute_prems to underlie defer_tac and rotate_prems
|
#
7fd0670a |
|
23-Jul-1999 |
wenzelm <none@none> |
tuned add_term_varnames;
|
#
23f769d0 |
|
08-Jul-1999 |
wenzelm <none@none> |
improved error msgs of instantiate;
|
#
252f6942 |
|
06-Jul-1999 |
wenzelm <none@none> |
added clear_mss;
|
#
b6dc8bb9 |
|
05-Jun-1999 |
wenzelm <none@none> |
varifyT': observe additional 'fixed' tfrees;
|
#
3ab70f1a |
|
29-Apr-1999 |
nipkow <none@none> |
Eta contraction is now performed all the time during rewriting.
|
#
77c35c2e |
|
17-Mar-1999 |
wenzelm <none@none> |
qualify Theory.sign_of etc.;
|
#
c50c6a31 |
|
17-Mar-1999 |
wenzelm <none@none> |
added def_name; class_triv: Sign.sg;
|
#
8c92d959 |
|
12-Jan-1999 |
wenzelm <none@none> |
signature BASIC_THM; theorem / axiom deriv: added tags; get/put_name_tags; type attribute;
|
#
0ee62235 |
|
08-Oct-1998 |
nipkow <none@none> |
Further improvement of the simplifier.
|
#
834db941 |
|
07-Oct-1998 |
nipkow <none@none> |
Tuned simplifier not to re-normalized already normalized terms.
|
#
d484c644 |
|
18-Sep-1998 |
paulson <none@none> |
improved error messages
|
#
382ca194 |
|
19-Aug-1998 |
wenzelm <none@none> |
assume: adjust_maxidx;
|
#
4db6c812 |
|
19-Aug-1998 |
paulson <none@none> |
The warning "Rewrite rule from different theory" is ALWAYS printed, even if tracing is off.
|
#
6e0b7f20 |
|
05-Jun-1998 |
wenzelm <none@none> |
Object.T;
|
#
b49cdbe8 |
|
29-Apr-1998 |
wenzelm <none@none> |
tuned get_ax (uses ancestry); added get_def: theory -> xstring -> thm;
|
#
aa959df4 |
|
22-Apr-1998 |
nipkow <none@none> |
Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching.
|
#
f426b4c8 |
|
04-Apr-1998 |
wenzelm <none@none> |
tuned trace msgs;
|
#
676dde0d |
|
11-Mar-1998 |
nipkow <none@none> |
Made mutual simplification of prems a special case.
|
#
d5b5614b |
|
10-Mar-1998 |
nipkow <none@none> |
Asm_full_simp_tac now reorients asm c = t to t = c.
|
#
98b56688 |
|
10-Mar-1998 |
nipkow <none@none> |
New simplifier flag for mutual simplification.
|
#
6084a576 |
|
06-Mar-1998 |
nipkow <none@none> |
Removed superfluous `op'
|
#
786ed4df |
|
04-Mar-1998 |
nipkow <none@none> |
Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.
|
#
36cc27e4 |
|
28-Feb-1998 |
nipkow <none@none> |
Tried to reorganize rewriter a little. More to be done.
|
#
ed52c2aa |
|
30-Jan-1998 |
wenzelm <none@none> |
improved tracing of rewrite rule application;
|
#
d549312b |
|
19-Dec-1997 |
wenzelm <none@none> |
Term.termless;
|
#
df47432f |
|
12-Dec-1997 |
wenzelm <none@none> |
tuned msg;
|
#
e20c005f |
|
27-Nov-1997 |
wenzelm <none@none> |
removed read_cterms;
|
#
0a04d73e |
|
26-Nov-1997 |
wenzelm <none@none> |
added crep_cterm;
|
#
48e5cafa |
|
24-Nov-1997 |
nipkow <none@none> |
Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.
|
#
ce14539d |
|
21-Nov-1997 |
wenzelm <none@none> |
changed Sequence interface (now Seq, in seq.ML);
|
#
bc40b8db |
|
20-Nov-1997 |
wenzelm <none@none> |
added transfer_sg;
|
#
9eca2250 |
|
19-Nov-1997 |
wenzelm <none@none> |
tuned infer_types interface;
|
#
32f2a2af |
|
06-Nov-1997 |
wenzelm <none@none> |
deriv: eliminated references to theory;
|
#
0a8c6f5b |
|
04-Nov-1997 |
wenzelm <none@none> |
type object = exn (enhance readability);
|
#
f19cb486 |
|
03-Nov-1997 |
nipkow <none@none> |
logic: loops -> rewrite_rule_ok added rewrite_rule_extra_vars thm: Rewrite rules must not introduce new type vars on rhs. This lead to an incompleteness, is now banned, and the code has been simplified.
|
#
f5fb48b9 |
|
30-Oct-1997 |
nipkow <none@none> |
Modified trace output routines of simplifier.
|
#
a7863c26 |
|
30-Oct-1997 |
wenzelm <none@none> |
tuned simp trace;
|
#
6f8926b2 |
|
28-Oct-1997 |
wenzelm <none@none> |
added name_of_thm; improved name_thm: does not overwrite existing name;
|
#
ac1f0b46 |
|
24-Oct-1997 |
wenzelm <none@none> |
eq_thm (from drule.ML);
|
#
d17354e7 |
|
22-Oct-1997 |
wenzelm <none@none> |
tuned;
|
#
6467ca77 |
|
22-Oct-1997 |
wenzelm <none@none> |
tuned;
|
#
49b4ce08 |
|
21-Oct-1997 |
wenzelm <none@none> |
sg_ref: automatic adjustment of thms of draft theories;
|
#
c73b9067 |
|
16-Oct-1997 |
wenzelm <none@none> |
added transfer: theory -> thm -> thm;
|
#
6b5139e3 |
|
16-Oct-1997 |
nipkow <none@none> |
The simplifier has been improved a little: equations s=t which used to be rejected because of looping are now treated as (s=t) == True. The latter translation must be done outside of Thm because it involves the object-logic specific True. Therefore the simple loop test has been moved from Thm to Logic.
|
#
bf8dee95 |
|
09-Oct-1997 |
wenzelm <none@none> |
fixed get_axiom, invoke_oracle; improved Oracle deriv;
|
#
c746d214 |
|
06-Oct-1997 |
wenzelm <none@none> |
tuned read_cterms;
|
#
1c7875f1 |
|
25-Jul-1997 |
wenzelm <none@none> |
added prems argument to simplification procedures;
|
#
85980ad9 |
|
23-Jul-1997 |
paulson <none@none> |
Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.
|
#
efa33404 |
|
23-Jul-1997 |
wenzelm <none@none> |
improved simp tracing;
|
#
a7c1f385 |
|
22-Jul-1997 |
wenzelm <none@none> |
added dest_mss, merge_mss; fixed matching of simproc lhss;
|
#
da71d20d |
|
18-Jul-1997 |
wenzelm <none@none> |
tuned warning; improved comments;
|
#
cc8416fb |
|
05-Jun-1997 |
paulson <none@none> |
freezeT now refers to Type.freeze_thaw
|
#
5e53eff2 |
|
25-Apr-1997 |
wenzelm <none@none> |
improved tmp comment;
|
#
cd6322f5 |
|
24-Apr-1997 |
nipkow <none@none> |
rename_params_rule used to check if the new name clashed with a free name in the whole goal state. Now checks only the subgoal concerned.
|
#
0ccb6de1 |
|
23-Apr-1997 |
wenzelm <none@none> |
simprocs called with eta contracted subterm;
|
#
3421b905 |
|
17-Apr-1997 |
wenzelm <none@none> |
improved type check error messages;
|
#
5dd18191 |
|
16-Apr-1997 |
wenzelm <none@none> |
Sorts.str_of_sort;
|
#
4d798205 |
|
14-Mar-1997 |
nipkow <none@none> |
Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.
|
#
f196d881 |
|
21-Feb-1997 |
paulson <none@none> |
Introduction of rotate_rule
|
#
a9963385 |
|
15-Feb-1997 |
oheimb <none@none> |
added del_congs
|
#
e7aa18a1 |
|
13-Feb-1997 |
nipkow <none@none> |
Made troublesome simplifier warning dependent on trace_simp.
|
#
99b64bfd |
|
22-Jan-1997 |
nipkow <none@none> |
Added warning msg when the simplifier cannot use a premise as a rewrite rule because it contains (type) unknowns.
|
#
c502bc87 |
|
16-Jan-1997 |
wenzelm <none@none> |
added termless parameter; added simplification procedures;
|
#
199e4752 |
|
13-Dec-1996 |
wenzelm <none@none> |
fixed warning;
|
#
a03b75ec |
|
28-Nov-1996 |
paulson <none@none> |
Replaced map...~~ by ListPair.map
|
#
1527b532 |
|
18-Nov-1996 |
paulson <none@none> |
Changed subst_bounds to subst_bound, to run faster
|
#
b57eae9d |
|
13-Nov-1996 |
paulson <none@none> |
Removal of polymorphic equality via mem, subset, eq_set, etc
|
#
add83b84 |
|
12-Nov-1996 |
paulson <none@none> |
Changed some mem, ins and union calls to be monomorphic
|
#
6c780d75 |
|
05-Nov-1996 |
wenzelm <none@none> |
tuned fix_shyps a little bit more;
|
#
3bc11069 |
|
01-Nov-1996 |
paulson <none@none> |
Now uses Int.max instead of max nodup_Vars now updates maxidx
|
#
bdb7f70e |
|
30-Oct-1996 |
paulson <none@none> |
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
|
#
1a576a65 |
|
01-Oct-1996 |
wenzelm <none@none> |
added shyps comment;
|
#
28a46107 |
|
30-Sep-1996 |
nipkow <none@none> |
Inserted check for rewrite rules which introduce extra Vars on the rhs.
|
#
e8d10f19 |
|
28-Jun-1996 |
paulson <none@none> |
Added type-checking to rule "combination". This corrects a fault concerning soundness. See Jeremy Dawsons message of 27 Jun 1996 on isabelle-users
|
#
c0b81f1d |
|
13-Jun-1996 |
paulson <none@none> |
Now del_simp catches the right exception!
|
#
ad495bdc |
|
29-Apr-1996 |
clasohm <none@none> |
moved dest_cimplies to drule.ML; added adjust_maxidx
|
#
7858cae1 |
|
17-Apr-1996 |
oheimb <none@none> |
*** empty log message ***
|
#
2850d278 |
|
03-Apr-1996 |
nipkow <none@none> |
Plugged some more loopholes with nodup_Vars.
|
#
e0b30b24 |
|
21-Mar-1996 |
paulson <none@none> |
name_thm no longer takes a theory argument, as the name no longer hides the previous derivation. Deleted sign_of_thm as redundant.
|
#
ef87df96 |
|
14-Mar-1996 |
berghofe <none@none> |
Added some functions which allow redirection of Isabelle's output
|
#
79b79e6d |
|
14-Mar-1996 |
berghofe <none@none> |
Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
|
#
4e1dd7da |
|
11-Mar-1996 |
nipkow <none@none> |
Non-matching congruence rule in rewriter is simply ignored. Used to cause error message.
|
#
fae577a2 |
|
11-Mar-1996 |
paulson <none@none> |
name_thm: now keeps the previous deriviation!
|
#
a4820292 |
|
05-Mar-1996 |
paulson <none@none> |
Addition of oracles
|
#
fdcfb3c9 |
|
01-Mar-1996 |
paulson <none@none> |
Addition of proof objects
|
#
b0170ea2 |
|
22-Feb-1996 |
clasohm <none@none> |
added cabs and crep_thm
|
#
c66c0f9d |
|
21-Feb-1996 |
clasohm <none@none> |
removed mk_prop; added capply; simplified dest_abs
|
#
85c404ff |
|
16-Feb-1996 |
paulson <none@none> |
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
|
#
aa0dda80 |
|
13-Feb-1996 |
nipkow <none@none> |
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
|
#
95c91aa7 |
|
12-Feb-1996 |
clasohm <none@none> |
added dest_comb, dest_abs and mk_prop for manipulating cterms
|
#
ecb6e3c2 |
|
29-Jan-1996 |
clasohm <none@none> |
inserted tabs again
|
#
385672e0 |
|
29-Jan-1996 |
clasohm <none@none> |
removed tabs
|
#
4c54da09 |
|
22-Dec-1995 |
paulson <none@none> |
Commented the datatype declaration of thm. Declared compress: thm -> thm to copy a thm and maximize sharing in it. "ext_axms" now calls Term.compress_term so that stored axioms use sharing.
|
#
fc1029fe |
|
08-Dec-1995 |
paulson <none@none> |
New function read_cterms is a combination of read_def_cterm and read_cterm. It reads and simultaneously type-checks a list of strings. cterm_of no longer catches exception TYPE; instead it must be caught later on and a message printed using Sign.exn_type_msg. More informative messages can be printed this way.
|
#
e6877d8b |
|
21-Sep-1995 |
wenzelm <none@none> |
bicompose_aux: tuned fix_shyps; simplifier: fixed handling of shyps;
|
#
75676ca0 |
|
01-Sep-1995 |
wenzelm <none@none> |
considerably tuned shyps handling;
|
#
34d9c81f |
|
17-Aug-1995 |
nipkow <none@none> |
deactivated fix_shyps.
|
#
59452d21 |
|
01-Aug-1995 |
wenzelm <none@none> |
MAJOR changes: added shyps component to type thm; added rules strip_shyps, implies_intr_shyps; fixed rules to handle shyps properly;
|
#
a4cebceb |
|
25-Jul-1995 |
lcp <none@none> |
match_bvs no longer puts a name in the alist if it is null ("")
|
#
0bc4ecc0 |
|
26-Jun-1995 |
wenzelm <none@none> |
added add_trrules_i; cleaned up signature THM; improved some comments;
|
#
42af5067 |
|
16-Apr-1995 |
nipkow <none@none> |
Fixed old bug in the simplifier. Term to be simplified now carries around its maxidx. Needed for renaming rewrite or congruence rules. maxidx should be ~1 in most cases (ie no Vars), hence reasonable overhead.
|
#
b9912d18 |
|
10-Apr-1995 |
nipkow <none@none> |
Added comment to function "loops".
|
#
0515c872 |
|
10-Apr-1995 |
nipkow <none@none> |
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that the maxidx-filed of thms is computed correctly.
|
#
b30b44c0 |
|
29-Mar-1995 |
nipkow <none@none> |
Simplification: used Logic.occs instead of mem add_term_frees
|
#
5f323ce4 |
|
14-Mar-1995 |
clasohm <none@none> |
removed print_msg parameter of infer_types
|
#
c4fbfcef |
|
13-Mar-1995 |
nipkow <none@none> |
Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.
|
#
ac89311a |
|
03-Mar-1995 |
clasohm <none@none> |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
#
1480c01a |
|
16-Feb-1995 |
nipkow <none@none> |
Improved test for looping rewrite rules.
|
#
38f4bcaa |
|
08-Feb-1995 |
nipkow <none@none> |
Improved check for looping conditional rewrite rules.
|
#
dd2db51e |
|
09-Dec-1994 |
wenzelm <none@none> |
improved axioms_of: returns thms as the manual says;
|
#
eeae1192 |
|
21-Nov-1994 |
lcp <none@none> |
Pure/thm/norm_term_skip: new, for skipping normalization of the context Pure/thm/bicompose_aux: now computes nlift (number of lifted assumptions in new subgoals) and avoids normalizing the first nlift assumptions in the case where the proof state is not affected. Pure/thm/norm_term_skip: now normalizes types of parameters Pure/thm/THM: aligned colons
|
#
7a56034b |
|
02-Nov-1994 |
nipkow <none@none> |
Modified pattern.ML to perform proper matching of Higher-Order Patterns. Modified thm.ML to preserve bound var names during rewriting. Renamed eta_matches to matches.
|
#
8d687a4a |
|
28-Oct-1994 |
nipkow <none@none> |
Prepared the code for preservation of bound var names during rewriting. Still requires a matching function for HO-patterns.
|
#
1d63784f |
|
04-Oct-1994 |
clasohm <none@none> |
added print_msg; added call of Type.infer_types to resolve ambiguities
|
#
7d0aa6a1 |
|
27-Sep-1994 |
nipkow <none@none> |
Modified termord to take account of the Abs-Abs case.
|
#
420c6dd2 |
|
23-Aug-1994 |
wenzelm <none@none> |
read_def_cterm: minor changes; merge_thm_sgs: improved error msg;
|
#
50ef55cf |
|
19-Aug-1994 |
wenzelm <none@none> |
added inferT_axm; removed extend_theory; changed read_def_cterm: now uses Sign.infer_types;
|
#
750e9c1c |
|
19-Jul-1994 |
wenzelm <none@none> |
fixed comment: "(| _ : _ |)" to "OFCLASS(_, _)"
|
#
d82c5b16 |
|
01-Jul-1994 |
clasohm <none@none> |
rewritec now uses trace_thm for it's "rewrite rule from different theory" message
|
#
159cee0e |
|
19-Jun-1994 |
nipkow <none@none> |
Improved error msg "Proved wrong thm"
|
#
f9a2e5c5 |
|
17-Jun-1994 |
nipkow <none@none> |
ordered rewriting applies to conditional rules as well now
|
#
352d47d7 |
|
15-Jun-1994 |
wenzelm <none@none> |
added add_classrel;
|
#
f2959af1 |
|
29-May-1994 |
nipkow <none@none> |
Internale optimization of the simplifier: in case a subterm stays unchanged, None is returned. Speeds things up a little bit and is going to be useful later on.
|
#
f58b7426 |
|
26-May-1994 |
wenzelm <none@none> |
added class_triv: theory -> class -> thm (for axclasses); renamed ext_axtab to new_axioms; restored functor sig constraint :THM;
|
#
c9f7973d |
|
19-May-1994 |
wenzelm <none@none> |
new datatype theory, supports 'draft theories' and incremental extension: add_classes, add_defsort, add_types, add_tyabbrs, add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax, add_syntax_i, add_trfuns, add_trrules, add_axioms, add_axioms_i, add_thyname; added merge_thy_list for multiple merges and extend-merges; added rep_theory, subthy, eq_thy, cert_axm, read_axm; changed type of axioms_of; renamed internal merge_theories to merge_thm_sgs; various internal changes of thm and theory related code;
|
#
f317eebf |
|
06-Apr-1994 |
lcp <none@none> |
restored the signature constraint :THM
|
#
7ec9a34a |
|
26-Mar-1994 |
nipkow <none@none> |
Changed term ordering for permutative rewrites to be AC-compatible.
|
#
494feb3b |
|
22-Mar-1994 |
nipkow <none@none> |
Implemented "ordered rewriting": rules which merely permute variables, such as commutativity, are only applied if the term becaomes lexicographically smaller (according to some fixed ordering on the term structure).
|
#
945c6819 |
|
01-Mar-1994 |
nipkow <none@none> |
deleted a comment
|
#
72c7fae6 |
|
03-Feb-1994 |
wenzelm <none@none> |
extend_theory: changed type of "abbrs" arg; added cterm_fun, read_ctyp (from drule.ML); ctyp_of, cterm_of, etc.: now use Sign.certify_...; assumption: now uses Envir.is_empty; bicompose_aux: fixed BUG (unifier with empty "asol" but non-empty "iTs" wasn't applied); fixed axioms_of;
|
#
47d08d8c |
|
19-Jan-1994 |
wenzelm <none@none> |
commented out sig constraint of functor (for debugging purposes);
|
#
3d95653e |
|
18-Jan-1994 |
lcp <none@none> |
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field of a theorem to be regarded as a cterm -- avoids expensive calls to cterm_of.
|
#
a0f6f37f |
|
14-Jan-1994 |
nipkow <none@none> |
optimized net for matching of abstractions to speed up simplifier
|
#
4f17ad41 |
|
11-Jan-1994 |
nipkow <none@none> |
optimized the number of eta-contractions in rewriting
|
#
4fdd85fc |
|
10-Jan-1994 |
wenzelm <none@none> |
commented out sig constraint of functor (for debugging purposes);
|
#
9d5f6c26 |
|
05-Jan-1994 |
nipkow <none@none> |
added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.
|
#
f684618d |
|
04-Jan-1994 |
nipkow <none@none> |
changed tracing of simplifier
|
#
f67cfc99 |
|
02-Jan-1994 |
nipkow <none@none> |
optimized simplifier - signature of rewritten term stays constant
|
#
4a875979 |
|
21-Dec-1993 |
nipkow <none@none> |
Necessary changes to accomodate type abbreviations.
|
#
95668403 |
|
10-Dec-1993 |
nipkow <none@none> |
updated instantiate to deal with type clashes
|
#
b34944be |
|
22-Nov-1993 |
nipkow <none@none> |
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
|
#
6420b481 |
|
11-Nov-1993 |
nipkow <none@none> |
Changed the simplifier: if the subgoaler proves an unexpected thm, chances are, it is an instance of the expected thm. Instead of aborting, rewriting now fails at that point.
|
#
6964436f |
|
29-Oct-1993 |
nipkow <none@none> |
added function del_simps
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|