#
34ca367d |
|
08-Nov-2019 |
wenzelm <none@none> |
clarified modules;
|
#
4cca32c1 |
|
04-Nov-2019 |
wenzelm <none@none> |
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
|
#
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;
|
#
51e1b2b2 |
|
03-Nov-2019 |
wenzelm <none@none> |
clarified modules;
|
#
8243f707 |
|
02-Nov-2019 |
wenzelm <none@none> |
tuned signature;
|
#
9f2472c6 |
|
22-Oct-2019 |
wenzelm <none@none> |
more conservative type names, e.g. relevant for Isabelle/MMT export;
|
#
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;
|
#
d644b6b4 |
|
20-Oct-2019 |
wenzelm <none@none> |
option to export standardized proof terms (not scalable);
|
#
2d7677d5 |
|
11-Oct-2019 |
wenzelm <none@none> |
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
|
#
5954cb84 |
|
11-Oct-2019 |
wenzelm <none@none> |
clarified signature;
|
#
438cc573 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
688e1181 |
|
03-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
aede6033 |
|
02-Aug-2019 |
wenzelm <none@none> |
clarified modules: inference kernel maintains sort algebra within the logic;
|
#
cc49f21e |
|
30-Jul-2019 |
wenzelm <none@none> |
clarified global theory context;
|
#
bec922a7 |
|
30-Jul-2019 |
wenzelm <none@none> |
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
|
#
c38b8b65 |
|
30-Jul-2019 |
wenzelm <none@none> |
clarified context;
|
#
90e0a6db |
|
30-Jul-2019 |
wenzelm <none@none> |
clarified modules;
|
#
82dd600e |
|
24-Jul-2019 |
wenzelm <none@none> |
clarified modules;
|
#
c93a1841 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned signature;
|
#
95f3ac48 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned;
|
#
756fcf77 |
|
13-Apr-2019 |
wenzelm <none@none> |
tuned signature -- more ctyp operations;
|
#
0e5c06bc |
|
03-Jan-2019 |
wenzelm <none@none> |
clarified signature: more types;
|
#
87409fcf |
|
25-Apr-2018 |
wenzelm <none@none> |
tuned -- avoid spurious exception trace for "the";
|
#
28b398a3 |
|
07-Mar-2018 |
wenzelm <none@none> |
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
|
#
e614198e |
|
25-Feb-2018 |
wenzelm <none@none> |
prefer symbols;
|
#
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap; tuned comments;
|
#
bd3048b2 |
|
21-Feb-2018 |
wenzelm <none@none> |
explicit operations to instantiate frees: typ, term, thm, morphism;
|
#
1a8829cb |
|
19-Feb-2018 |
wenzelm <none@none> |
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes; register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel); support for lazy notes for locale activation (still inactive);
|
#
ba9cb2ae |
|
18-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
#
17fc044a |
|
01-Feb-2018 |
wenzelm <none@none> |
clarified signature;
|
#
f30be3c8 |
|
22-Jun-2017 |
wenzelm <none@none> |
consolidate proofs more simultaneously;
|
#
151b7ea2 |
|
10-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
#
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;
|
#
e33b0cb4 |
|
14-Dec-2016 |
wenzelm <none@none> |
more careful derivation_closed / close_derivation;
|
#
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
#
bee57ad5 |
|
23-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
#
7f175f96 |
|
25-Apr-2016 |
wenzelm <none@none> |
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
|
#
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
#
a279bbf2 |
|
16-Dec-2015 |
wenzelm <none@none> |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
#
82270f93 |
|
15-Dec-2015 |
wenzelm <none@none> |
tuned signature -- clarified modules;
|
#
cefac6f0 |
|
23-Oct-2015 |
wenzelm <none@none> |
print thm wrt. local shyps (from full proof context); tuned;
|
#
82b464e3 |
|
23-Oct-2015 |
wenzelm <none@none> |
clarified modules; tuned signature;
|
#
24e5eb9a |
|
06-Oct-2015 |
wenzelm <none@none> |
added Thm.forall_intr_name;
|
#
917ba2d0 |
|
06-Oct-2015 |
wenzelm <none@none> |
just one theorem kind, which is legacy anyway;
|
#
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
#
88a29a83 |
|
25-Sep-2015 |
wenzelm <none@none> |
tuned;
|
#
6033868f |
|
25-Sep-2015 |
wenzelm <none@none> |
tuned signature: eliminated pointless type Context.pretty;
|
#
a152ef96 |
|
24-Sep-2015 |
wenzelm <none@none> |
more explicit Defs.context: use proper name spaces as far as possible;
|
#
63d9e25c |
|
30-Aug-2015 |
wenzelm <none@none> |
trim context for persistent storage;
|
#
f063bb8d |
|
28-Aug-2015 |
wenzelm <none@none> |
tuned;
|
#
940daa43 |
|
28-Aug-2015 |
wenzelm <none@none> |
tuned;
|
#
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;
|
#
e9e8258e |
|
16-Aug-2015 |
wenzelm <none@none> |
tuned;
|
#
02f6d501 |
|
16-Aug-2015 |
wenzelm <none@none> |
prefer theory_id operations; tuned signature;
|
#
57b4c9d7 |
|
15-Aug-2015 |
wenzelm <none@none> |
clarified context;
|
#
e3afad2b |
|
28-Jul-2015 |
wenzelm <none@none> |
more explicit context; tuned signature;
|
#
01b39a18 |
|
28-Jul-2015 |
wenzelm <none@none> |
eliminated dead code;
|
#
eaa96fee |
|
28-Jul-2015 |
wenzelm <none@none> |
more direct access to atomic cterms;
|
#
92acade0 |
|
28-Jul-2015 |
wenzelm <none@none> |
proper context;
|
#
0226e5de |
|
28-Jul-2015 |
wenzelm <none@none> |
more direct access to atomic cterms;
|
#
dd91653e |
|
28-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
#
c2232610 |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature; clarified context;
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
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);
|
#
c431d096 |
|
03-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
#
8f453cab |
|
01-Jun-2015 |
wenzelm <none@none> |
tuned;
|
#
6e829806 |
|
08-Apr-2015 |
wenzelm <none@none> |
explicitly checked alpha conversion -- actual renaming happens outside kernel;
|
#
e7b7ba43 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
04cfe663 |
|
05-Mar-2015 |
wenzelm <none@none> |
tuned -- more explicit use of context;
|
#
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};
|
#
4a5721b5 |
|
18-Aug-2014 |
wenzelm <none@none> |
more general dummy: may contain "parked arguments", for example;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
03233c38 |
|
20-Feb-2014 |
wenzelm <none@none> |
clarified printing of undeclared hyps;
|
#
9f54675a |
|
17-Feb-2014 |
wenzelm <none@none> |
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
|
#
85905246 |
|
11-Jan-2014 |
wenzelm <none@none> |
check_hyps when attributes are applied;
|
#
3260066f |
|
11-Jan-2014 |
wenzelm <none@none> |
check_hyps for attribute application (still inactive, due to non-compliant tools); bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;
|
#
db965533 |
|
10-Jan-2014 |
wenzelm <none@none> |
more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
|
#
5cfa97d1 |
|
26-Aug-2013 |
wenzelm <none@none> |
always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);
|
#
ba320d4b |
|
17-Jul-2013 |
wenzelm <none@none> |
more official Thm.eq_thm_strict, without demanding ML equality type;
|
#
44d437c3 |
|
28-Feb-2013 |
wenzelm <none@none> |
discontinued empty name bindings in 'axiomatization';
|
#
6141f390 |
|
01-Sep-2012 |
wenzelm <none@none> |
discontinued complicated/unreliable notion of recent proofs within context;
|
#
d612353e |
|
31-Aug-2012 |
wenzelm <none@none> |
tuned signature;
|
#
91fcdd2b |
|
30-Aug-2012 |
wenzelm <none@none> |
some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
|
#
69fc4752 |
|
30-Aug-2012 |
wenzelm <none@none> |
tuned signature;
|
#
5b99cf15 |
|
10-Mar-2012 |
wenzelm <none@none> |
eliminated dead code;
|
#
5841f507 |
|
07-Mar-2012 |
wenzelm <none@none> |
tuned signature;
|
#
f2cf0c71 |
|
03-Mar-2012 |
wenzelm <none@none> |
canonical argument order for attribute application;
|
#
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;
|
#
f50bbdc8 |
|
06-Nov-2011 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
9fa04411 |
|
06-Nov-2011 |
wenzelm <none@none> |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
|
#
38dc694f |
|
12-Jul-2011 |
wenzelm <none@none> |
more uniform Properties in ML and Scala;
|
#
b6f9ad57 |
|
09-Jun-2011 |
wenzelm <none@none> |
tuned signature: Name.invent and Name.invent_names;
|
#
e64a40eb |
|
26-Apr-2011 |
wenzelm <none@none> |
mark thm tag "kind" as legacy;
|
#
7685bb05 |
|
20-Apr-2011 |
wenzelm <none@none> |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
#
13a7cd41 |
|
17-Apr-2011 |
wenzelm <none@none> |
report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
|
#
8dc52649 |
|
28-Oct-2010 |
wenzelm <none@none> |
type attribute is derived concept outside the kernel;
|
#
d5fed4bd |
|
05-Sep-2010 |
wenzelm <none@none> |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
#
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;
|
#
f3757455 |
|
11-Apr-2010 |
wenzelm <none@none> |
Thm.add_axiom/add_def: return internal name of foundational axiom;
|
#
87866196 |
|
27-Mar-2010 |
wenzelm <none@none> |
disallow premises in primitive Theory.add_def -- handle in Thm.add_def; eliminated obsolete Sign.cert_def; misc tuning and clarification;
|
#
330ecb2e |
|
27-Mar-2010 |
wenzelm <none@none> |
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
|
#
15ec9fdf |
|
21-Mar-2010 |
wenzelm <none@none> |
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
|
#
b008c2e5 |
|
21-Mar-2010 |
wenzelm <none@none> |
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises; more uniform add_axiom/add_def;
|
#
6770f7bb |
|
21-Mar-2010 |
wenzelm <none@none> |
more explicit invented name;
|
#
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;
|
#
0ab1ed86 |
|
11-Mar-2010 |
wenzelm <none@none> |
tuned;
|
#
e3d0611a |
|
27-Feb-2010 |
wenzelm <none@none> |
modernized structure Term_Ord;
|
#
227c8de0 |
|
19-Feb-2010 |
wenzelm <none@none> |
Thm.def_binding;
|
#
ed336432 |
|
16-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete thm position stuff;
|
#
105f07d1 |
|
15-Nov-2009 |
wenzelm <none@none> |
tuned;
|
#
28c1be77 |
|
13-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
#
cd3b830c |
|
12-Nov-2009 |
wenzelm <none@none> |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
#
d4527641 |
|
12-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
#
439813d7 |
|
05-Nov-2009 |
wenzelm <none@none> |
scalable version of Named_Thms, using Item_Net;
|
#
aa223bae |
|
01-Nov-2009 |
wenzelm <none@none> |
adapted Item_Net; tuned;
|
#
32b046a5 |
|
29-Oct-2009 |
wenzelm <none@none> |
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
|
#
47a6fbab |
|
25-Oct-2009 |
wenzelm <none@none> |
maintain group via name space, not tags;
|
#
e98e5682 |
|
01-Oct-2009 |
wenzelm <none@none> |
added Ctermtab, cterm_cache, thm_cache; tuned;
|
#
4dbd862f |
|
29-Jul-2009 |
wenzelm <none@none> |
added certify_inst, certify_instantiate;
|
#
3dbff3fc |
|
26-Jul-2009 |
wenzelm <none@none> |
lambda/cabs/all: named variants;
|
#
196435a0 |
|
09-Jul-2009 |
wenzelm <none@none> |
renamed structure TermSubst to Term_Subst;
|
#
b063764f |
|
09-Jul-2009 |
wenzelm <none@none> |
renamed functor TableFun to Table, and GraphFun to Graph;
|
#
bad90cf2 |
|
06-Jul-2009 |
wenzelm <none@none> |
clarified strip_shyps: proper type witnesses for present sorts; moved fold_terms to thm.ML;
|
#
5e95080e |
|
06-Jul-2009 |
wenzelm <none@none> |
clarified Thm.of_class/of_sort/class_triv;
|
#
836440db |
|
02-Jul-2009 |
wenzelm <none@none> |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
#
e9ec6b63 |
|
18-May-2009 |
haftmann <none@none> |
introduced Thm.generatedK
|
#
155bffcd |
|
16-May-2009 |
bulwahn <none@none> |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
#
eecc5601 |
|
17-Mar-2009 |
wenzelm <none@none> |
tuned comment;
|
#
dee1f92e |
|
17-Mar-2009 |
wenzelm <none@none> |
adapted to general Item_Net;
|
#
67716b50 |
|
11-Mar-2009 |
wenzelm <none@none> |
added def_binding_optional -- robust version of def_name_optional for bindings;
|
#
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;
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
2bc3a0c2 |
|
03-Mar-2009 |
wenzelm <none@none> |
added type binding and val empty_binding;
|
#
5061c2dd |
|
21-Jan-2009 |
haftmann <none@none> |
binding replaces bstring
|
#
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
4e5786a4 |
|
23-Oct-2008 |
wenzelm <none@none> |
renamed Thm.get_axiom_i to Thm.axiom;
|
#
42be30c5 |
|
16-Oct-2008 |
wenzelm <none@none> |
added check_shyps, which reject pending sort hypotheses;
|
#
bc4d2ebb |
|
03-Sep-2008 |
wenzelm <none@none> |
simplified add_axiom: no hyps;
|
#
d0b84733 |
|
27-Aug-2008 |
wenzelm <none@none> |
type Properties.T;
|
#
96ff5c41 |
|
14-Aug-2008 |
wenzelm <none@none> |
moved basic thm operations from structure PureThy to Thm; added position operations; tuned;
|
#
66ce2bc4 |
|
18-Jun-2008 |
wenzelm <none@none> |
removed obsolete read_def_cterms/read_cterm;
|
#
4fd826a1 |
|
15-Apr-2008 |
wenzelm <none@none> |
Theory.eq_thy;
|
#
d4aa0c76 |
|
15-Apr-2008 |
wenzelm <none@none> |
Thm.forall_elim_var(s);
|
#
0fa34d21 |
|
12-Apr-2008 |
wenzelm <none@none> |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
#
3f17f715 |
|
03-Dec-2007 |
haftmann <none@none> |
interface for unchecked definitions
|
#
8b1f9d35 |
|
11-Oct-2007 |
wenzelm <none@none> |
added elim_implies (more convenient argument order); added unvarify (from drule.ML); added specification primitives: add_axiom, add_def;
|
#
cdf7a773 |
|
10-Oct-2007 |
wenzelm <none@none> |
tuned;
|
#
af393012 |
|
30-Sep-2007 |
wenzelm <none@none> |
Markup.internalK;
|
#
5e93d637 |
|
29-Jul-2007 |
wenzelm <none@none> |
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;
|
#
68a27605 |
|
05-Jul-2007 |
wenzelm <none@none> |
added is_reflexive;
|
#
0cdede9e |
|
24-Jun-2007 |
wenzelm <none@none> |
added reasonably efficient add_cterm_frees;
|
#
f55b9edc |
|
31-May-2007 |
wenzelm <none@none> |
made aconvc pervasive;
|
#
1a80356f |
|
31-May-2007 |
wenzelm <none@none> |
moved aconvc to more_thm.ML;
|
#
4a61e59d |
|
09-May-2007 |
wenzelm <none@none> |
added destructors from drule.ML; added mk_binop;
|
#
366a0a39 |
|
15-Apr-2007 |
wenzelm <none@none> |
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
|
#
981b1d30 |
|
14-Apr-2007 |
wenzelm <none@none> |
added read_def_cterms, read_cterm (from thm.ML);
|
#
3d59f582 |
|
28-Feb-2007 |
wenzelm <none@none> |
tuned;
|
#
3387a5ae |
|
26-Feb-2007 |
wenzelm <none@none> |
Further operations on type thm, outside the inference kernel.
|