#
4d8b7cc9 |
|
13-Mar-2020 |
wenzelm <none@none> |
some uses of "' " as witness for this feature;
|
#
34ddd120 |
|
23-Nov-2019 |
wenzelm <none@none> |
clarified signature;
|
#
d84471da |
|
24-Jul-2019 |
wenzelm <none@none> |
avoid global syntax for MinProof (amending e31271559de8);
|
#
fe9eef5c |
|
21-Jul-2019 |
wenzelm <none@none> |
global declaration of abstract syntax for proof terms, with qualified names; clarified modules;
|
#
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap; tuned comments;
|
#
3b5cb23d |
|
24-Feb-2018 |
wenzelm <none@none> |
notation for dummy sort;
|
#
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
#
7c8192ef |
|
04-Aug-2016 |
wenzelm <none@none> |
prefer hardwired "nothing";
|
#
772cb5d0 |
|
01-Apr-2016 |
wenzelm <none@none> |
explicit property for unbreakable block;
|
#
55c785b8 |
|
30-Mar-2016 |
wenzelm <none@none> |
clarified simple mixfix;
|
#
6ad8d4d8 |
|
29-Mar-2016 |
wenzelm <none@none> |
more position information for type mixfix;
|
#
9b94c25b |
|
06-Mar-2016 |
wenzelm <none@none> |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
#
ea008a30 |
|
08-Jan-2016 |
wenzelm <none@none> |
discontinued \<struct> syntax;
|
#
3a7ad270 |
|
29-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; uniform syntax for Pure.imp; removed obsolete "HTML" syntax;
|
#
a0dc69c0 |
|
22-Sep-2015 |
wenzelm <none@none> |
tuned signature;
|
#
8ed115e9 |
|
22-Sep-2015 |
wenzelm <none@none> |
eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
|
#
13bb5ba7 |
|
22-Sep-2015 |
wenzelm <none@none> |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
|
#
a352ac5a |
|
09-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon> from syntax of constraints;
|
#
17db18c6 |
|
22-Sep-2014 |
wenzelm <none@none> |
discontinued old "xnum" token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via "num" with mixfix grammar; recovered printing of ZF numerals: "one" is abbreviation;
|
#
92c442b3 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
4a6d4dcb |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
d3dc194f |
|
20-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
81d6c2a2 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
88385dd9 |
|
21-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
bad7e22c |
|
21-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
6dc01e59 |
|
20-Mar-2014 |
wenzelm <none@none> |
produce qualified names more directly;
|
#
c5699b5f |
|
22-Jan-2014 |
wenzelm <none@none> |
inner syntax token language allows regular quoted strings; tuned signature;
|
#
42b5b84f |
|
18-Jan-2014 |
wenzelm <none@none> |
support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
|
#
a66c9494 |
|
23-Aug-2013 |
wenzelm <none@none> |
added Theory.setup convenience;
|
#
15932c08 |
|
28-May-2013 |
wenzelm <none@none> |
explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types;
|
#
8fa4b40e |
|
26-May-2013 |
wenzelm <none@none> |
tuned;
|
#
86bfbbb5 |
|
26-May-2013 |
wenzelm <none@none> |
tuned signature;
|
#
ffcd6989 |
|
25-May-2013 |
wenzelm <none@none> |
syntax translations always depend on context;
|
#
8b7cf9a2 |
|
03-Apr-2013 |
wenzelm <none@none> |
added var_position in analogy to longid_position, for typing reports on input; avoid duplicate token var report;
|
#
381e5d73 |
|
30-Dec-2012 |
wenzelm <none@none> |
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
|
#
d7a5acb6 |
|
19-Dec-2012 |
nipkow <none@none> |
removed odd associativity of ==
|
#
ee6246cd |
|
03-Oct-2012 |
wenzelm <none@none> |
allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;
|
#
e3f35e4e |
|
01-Oct-2012 |
wenzelm <none@none> |
report sort assignment of visible type variables;
|
#
96682752 |
|
15-Feb-2012 |
wenzelm <none@none> |
renamed "xstr" to "str_token";
|
#
8c8763eb |
|
16-Jan-2012 |
wenzelm <none@none> |
position constraints for numerals enable PIDE markup;
|
#
7085d004 |
|
30-Nov-2011 |
wenzelm <none@none> |
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
|
#
8c33a56f |
|
14-Nov-2011 |
wenzelm <none@none> |
inner syntax positions for string literals;
|
#
7a4c944d |
|
07-Nov-2011 |
wenzelm <none@none> |
discontinued numbered structure indexes (legacy feature);
|
#
525b491d |
|
22-Aug-2011 |
wenzelm <none@none> |
special treatment of structure index 1 in Pure, including legacy warning;
|
#
5a0ba8cd |
|
19-Apr-2011 |
wenzelm <none@none> |
less bulky "_position", for improved readability of parse trees;
|
#
13a7cd41 |
|
17-Apr-2011 |
wenzelm <none@none> |
report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
|
#
d94617f2 |
|
08-Apr-2011 |
wenzelm <none@none> |
discontinued Syntax.max_pri, which is not really a symbolic parameter;
|
#
85a20f7d |
|
08-Apr-2011 |
wenzelm <none@none> |
CONST syntax with positions;
|
#
b0a81ce3 |
|
08-Apr-2011 |
wenzelm <none@none> |
moved CONST syntax/translations to their proper place;
|
#
b77dcc9d |
|
08-Apr-2011 |
wenzelm <none@none> |
simplified Pure syntax bootstrap;
|
#
79e25c01 |
|
08-Apr-2011 |
wenzelm <none@none> |
renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;
|
#
c4f9ef65 |
|
08-Apr-2011 |
wenzelm <none@none> |
discontinued special treatment of structure Lexicon;
|
#
ecc6df14 |
|
08-Apr-2011 |
wenzelm <none@none> |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root; --HG-- rename : src/Pure/Syntax/syn_ext.ML => src/Pure/Syntax/syntax_ext.ML
|
#
1c017ad4 |
|
08-Apr-2011 |
wenzelm <none@none> |
explicit structure Syntax_Trans; discontinued old-style constrainAbsC; --HG-- rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML
|
#
f17b2df6 |
|
06-Apr-2011 |
wenzelm <none@none> |
type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
|
#
8fa04ea6 |
|
05-Apr-2011 |
wenzelm <none@none> |
moved unparse material to syntax_phases.ML;
|
#
83094238 |
|
22-Mar-2011 |
wenzelm <none@none> |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
#
e32a1cba |
|
22-Mar-2011 |
wenzelm <none@none> |
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;
|
#
308c65f5 |
|
20-Sep-2010 |
wenzelm <none@none> |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; --HG-- rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML
|
#
23d2ba43 |
|
17-Sep-2010 |
wenzelm <none@none> |
tuned signature of (Context_)Position.report variants;
|
#
6fcdee8b |
|
01-Sep-2010 |
wenzelm <none@none> |
actually declare "_constrainAbs" as @{syntax_const};
|
#
c25c5530 |
|
31-May-2010 |
wenzelm <none@none> |
modernized some structure names, keeping a few legacy aliases;
|
#
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;
|
#
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;
|
#
e2073456 |
|
21-Mar-2010 |
wenzelm <none@none> |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
#
952e731e |
|
21-Mar-2010 |
wenzelm <none@none> |
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
|
#
cd3f8037 |
|
02-Mar-2010 |
wenzelm <none@none> |
authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
|
#
d14717b0 |
|
21-Feb-2010 |
wenzelm <none@none> |
slightly more abstract syntax mark/unmark operations;
|
#
ed69a28a |
|
21-Feb-2010 |
wenzelm <none@none> |
authentic syntax for *all* term constants;
|
#
e8949437 |
|
16-Feb-2010 |
wenzelm <none@none> |
moved generic update_name to Pure syntax -- not specific to HOL/record;
|
#
d27c0f79 |
|
15-Feb-2010 |
wenzelm <none@none> |
renamed InfixName to Infix etc.;
|
#
e76659a1 |
|
15-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete thm position tags;
|
#
71833c27 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Theory_Data; tuned;
|
#
c9975fc3 |
|
02-Nov-2009 |
wenzelm <none@none> |
modernized structure Simple_Syntax;
|
#
1236ffba |
|
30-Oct-2009 |
haftmann <none@none> |
set Pure theory name properly
|
#
47a6fbab |
|
25-Oct-2009 |
wenzelm <none@none> |
maintain group via name space, not tags;
|
#
713fc456 |
|
24-Oct-2009 |
wenzelm <none@none> |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
#
348d0907 |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated dead code;
|
#
a2c3b772 |
|
21-Jul-2009 |
wenzelm <none@none> |
join_proofs: implicit exception; removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML; tuned;
|
#
11c617fc |
|
19-Jul-2009 |
wenzelm <none@none> |
cancel_proofs: some attempts at reworking group management (based on body promises only);
|
#
39a70e94 |
|
02-Apr-2009 |
wenzelm <none@none> |
tuned signature;
|
#
d206ad0e |
|
07-Mar-2009 |
wenzelm <none@none> |
more uniform handling of binding in targets and derived elements;
|
#
9ecd6ff9 |
|
06-Mar-2009 |
wenzelm <none@none> |
Theory.add_axioms/add_defs: replaced old bstring by binding;
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
0c02a0cf |
|
03-Mar-2009 |
wenzelm <none@none> |
Thm.binding;
|
#
d647eb14 |
|
01-Mar-2009 |
wenzelm <none@none> |
use long names for old-style fold combinators;
|
#
5061c2dd |
|
21-Jan-2009 |
haftmann <none@none> |
binding replaces bstring
|
#
2ad3cb5a |
|
10-Jan-2009 |
wenzelm <none@none> |
added cancel_proofs, based on task groups of "entered" proofs;
|
#
d24cc6b6 |
|
09-Jan-2009 |
wenzelm <none@none> |
tuned;
|
#
a83e548a |
|
09-Jan-2009 |
wenzelm <none@none> |
simplified join_proofs;
|
#
03049aab |
|
23-Dec-2008 |
wenzelm <none@none> |
renamed terminal category "float" to "float_token", to avoid name space conflicts with actual "float" types in user theories (only "float_const" is encountered in practice anyway); tuned;
|
#
38284ef6 |
|
05-Dec-2008 |
wenzelm <none@none> |
renamed force_proofs to join_proofs;
|
#
554fb94f |
|
04-Dec-2008 |
wenzelm <none@none> |
renamed type Lazy.T to lazy; force_proofs: original order;
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
740587ab |
|
01-Dec-2008 |
haftmann <none@none> |
new Binding module
|
#
1747dcf8 |
|
29-Nov-2008 |
nipkow <none@none> |
New lexical item "float".
|
#
9150bc5d |
|
20-Nov-2008 |
haftmann <none@none> |
fact table now using name bindings
|
#
3745db78 |
|
20-Nov-2008 |
haftmann <none@none> |
using name bindings
|
#
b08c2db5 |
|
19-Nov-2008 |
wenzelm <none@none> |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
#
646adbf1 |
|
18-Nov-2008 |
wenzelm <none@none> |
added force_proofs (based on thms ever passed through enter_thms);
|
#
4e5786a4 |
|
23-Oct-2008 |
wenzelm <none@none> |
renamed Thm.get_axiom_i to Thm.axiom;
|
#
d78e8640 |
|
16-Oct-2008 |
wenzelm <none@none> |
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
|
#
e3b24322 |
|
02-Sep-2008 |
wenzelm <none@none> |
name_thm etc.: pass position; note_thms etc.: Name.binding, report fact_decl;
|
#
2fac30b5 |
|
14-Aug-2008 |
wenzelm <none@none> |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
#
20732b72 |
|
05-Aug-2008 |
wenzelm <none@none> |
get_fact: report position;
|
#
88835ed7 |
|
04-Aug-2008 |
wenzelm <none@none> |
removed obsolete note_thms_cmd;
|
#
4da32258 |
|
29-Jul-2008 |
haftmann <none@none> |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
#
31c76652 |
|
24-Jul-2008 |
haftmann <none@none> |
dropped PureThy.note; added PureThy.add_thm
|
#
1333605e |
|
14-Jun-2008 |
wenzelm <none@none> |
removed old theorem database;
|
#
17ba4766 |
|
18-May-2008 |
wenzelm <none@none> |
theory Pure provides regular application syntax by default; added old_appl_syntax_setup for former Pure clients;
|
#
0b600516 |
|
16-Apr-2008 |
wenzelm <none@none> |
renamed check_fact to defined_fact;
|
#
45c76371 |
|
16-Apr-2008 |
wenzelm <none@none> |
removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;
|
#
d47eac5a |
|
15-Apr-2008 |
wenzelm <none@none> |
added intern_fact, check_fact, hide_fact; renamed all_facts_of to facts_of; removed hide_thms; Sign.hide_const;
|
#
8edaf447 |
|
15-Apr-2008 |
wenzelm <none@none> |
moved forall_elim_var(s) to more_thm.ML; get_thm(s) and hide_thms: use new table;
|
#
0ba04da2 |
|
12-Apr-2008 |
wenzelm <none@none> |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
#
783a6bf5 |
|
03-Apr-2008 |
wenzelm <none@none> |
removed obsolete add_axiomss(_i);
|
#
49d982c1 |
|
29-Mar-2008 |
wenzelm <none@none> |
eliminated destructive/critical theorem database; simplified store_thm(s); removed obsolete smart_store_thm(s); tuned;
|
#
0d38b565 |
|
28-Mar-2008 |
wenzelm <none@none> |
NAMED_CRITICAL;
|
#
55096917 |
|
28-Mar-2008 |
wenzelm <none@none> |
Context.>> : operate on Context.generic;
|
#
bea05653 |
|
27-Mar-2008 |
wenzelm <none@none> |
tuned;
|
#
d6b5c3a0 |
|
27-Mar-2008 |
wenzelm <none@none> |
removed obsolete appl_syntax, applC_syntax;
|
#
34beb830 |
|
27-Mar-2008 |
wenzelm <none@none> |
eliminated theory ProtoPure; implicit setup of emerging theory Pure;
|
#
6824d3d4 |
|
25-Mar-2008 |
wenzelm <none@none> |
get fact: do not compare names;
|
#
7bc11406 |
|
25-Mar-2008 |
wenzelm <none@none> |
support dynamic facts;
|
#
3dab2cfb |
|
20-Mar-2008 |
wenzelm <none@none> |
get_thms etc.: improved reporting of source position;
|
#
d488fd59 |
|
20-Mar-2008 |
wenzelm <none@none> |
Facts.Named: include position;
|
#
bb64f55b |
|
19-Mar-2008 |
wenzelm <none@none> |
simplified get_thm(s): back to plain name argument; renamed former get_thms(_silent) to get_fact(_silent);
|
#
a46b31e4 |
|
19-Mar-2008 |
wenzelm <none@none> |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
#
ea36c663 |
|
18-Mar-2008 |
wenzelm <none@none> |
removed check_lookup; added get_thms_silent;
|
#
0b7b9d02 |
|
18-Mar-2008 |
wenzelm <none@none> |
added ckeck_lookup flag (default false), which controls sanity check of thm lookup;
|
#
118bee97 |
|
17-Mar-2008 |
wenzelm <none@none> |
Facts.add_global;
|
#
2dc7785c |
|
15-Mar-2008 |
wenzelm <none@none> |
get_thm(s): check facts lookup vs. old thm database;
|
#
276adbc1 |
|
15-Mar-2008 |
wenzelm <none@none> |
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories); removed unused get_thm(s)_closure; removed obsolete fact_index_of, valid_thms, thms_containing(_consts);
|
#
4033d2fb |
|
10-Feb-2008 |
wenzelm <none@none> |
maintain default position;
|
#
567e2c2b |
|
26-Jan-2008 |
wenzelm <none@none> |
added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name;
|
#
ef52c05d |
|
10-Dec-2007 |
haftmann <none@none> |
added simple primitive note
|
#
2639fc9a |
|
13-Oct-2007 |
wenzelm <none@none> |
replaced obsolete Theory.add_finals_i by Theory.add_deps;
|
#
00cc8a4a |
|
11-Oct-2007 |
wenzelm <none@none> |
removed obsolete simple_def;
|
#
73f757c7 |
|
02-Oct-2007 |
wenzelm <none@none> |
removed unused add_defss;
|
#
0685a089 |
|
01-Oct-2007 |
wenzelm <none@none> |
NameSelection: more interval checks;
|
#
8d942da7 |
|
30-Sep-2007 |
wenzelm <none@none> |
Sign.add_consts_authentic: tags (Markup.property list);
|
#
c67687b3 |
|
25-Sep-2007 |
wenzelm <none@none> |
tuned functor application;
|
#
29d04fe6 |
|
27-Aug-2007 |
haftmann <none@none> |
added simple definition scheme
|
#
48550e57 |
|
13-Aug-2007 |
wenzelm <none@none> |
moved appl syntax to PureThy; SimpleSyntax.read_typ/term/prop;
|
#
2b54826d |
|
03-Aug-2007 |
wenzelm <none@none> |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
|
#
562784c6 |
|
28-Jul-2007 |
wenzelm <none@none> |
removed dead code;
|
#
9bed50ab |
|
23-Jul-2007 |
wenzelm <none@none> |
marked some CRITICAL sections;
|
#
792d3082 |
|
08-Jul-2007 |
wenzelm <none@none> |
thm tag: Markup.property list;
|
#
b62fe892 |
|
06-May-2007 |
wenzelm <none@none> |
simplified DataFun interfaces;
|
#
dda7c2a4 |
|
25-Apr-2007 |
wenzelm <none@none> |
renamed some old names Theory.xxx to Sign.xxx;
|
#
270b11bd |
|
26-Feb-2007 |
wenzelm <none@none> |
Thm.internalK;
|
#
ca75b915 |
|
26-Feb-2007 |
wenzelm <none@none> |
removed obsolete theorem_space;
|
#
662e7442 |
|
06-Feb-2007 |
wenzelm <none@none> |
added has_kind/get_kind; tuned;
|
#
afa3119e |
|
01-Feb-2007 |
wenzelm <none@none> |
proper use of PureThy.has_name_hint instead of hard-wired string'';
|
#
e023dc90 |
|
31-Jan-2007 |
aspinall <none@none> |
Expose hard-wired string which was changed and broke Proof General.
|
#
30200833 |
|
19-Jan-2007 |
wenzelm <none@none> |
moved thm/thms to ml_context.ML; moved generic_setup, add_oracle to isar_cmd.ML;
|
#
0f17da38 |
|
19-Jan-2007 |
wenzelm <none@none> |
adapted ML context operations;
|
#
bec0df8f |
|
30-Dec-2006 |
wenzelm <none@none> |
added has_name_hint; name_thm: more careful pre-naming;
|
#
b5dac97b |
|
04-Dec-2006 |
wenzelm <none@none> |
thm/prf: separate official name vs. additional tags;
|
#
d7088c07 |
|
30-Nov-2006 |
wenzelm <none@none> |
Theory.merge_list;
|
#
96060bb6 |
|
29-Nov-2006 |
wenzelm <none@none> |
*** bad commit -- reverted to previous version ***
|
#
a69047fa |
|
29-Nov-2006 |
wenzelm <none@none> |
added map/burrow_facts; exported name_multi, name_thm;
|
#
407fc559 |
|
28-Nov-2006 |
wenzelm <none@none> |
added map/burrow_facts; exported name_multi, name_thm;
|
#
3b63f941 |
|
27-Nov-2006 |
wenzelm <none@none> |
added burrow_fact; no export of name_thms(s);
|
#
b538f435 |
|
26-Nov-2006 |
wenzelm <none@none> |
updated (binder) syntax/notation;
|
#
8dede227 |
|
23-Nov-2006 |
wenzelm <none@none> |
tuned;
|
#
c823cd83 |
|
21-Nov-2006 |
wenzelm <none@none> |
moved theorem kinds from PureThy to Thm; exported note_thms(s);
|
#
1c390ba8 |
|
04-Oct-2006 |
haftmann <none@none> |
*** empty log message ***
|
#
fa18480a |
|
21-Sep-2006 |
wenzelm <none@none> |
member (op =);
|
#
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;
|
#
222e0624 |
|
05-Jun-2006 |
wenzelm <none@none> |
support embedded terms;
|
#
6e507eea |
|
12-May-2006 |
wenzelm <none@none> |
added add_defs_unchecked(_i);
|
#
661e7080 |
|
05-May-2006 |
wenzelm <none@none> |
added syntax for _type_constraint_;
|
#
cf09f0e2 |
|
27-Apr-2006 |
wenzelm <none@none> |
tuned basic list operators (flat, maps, map_filter);
|
#
d4a1d64e |
|
26-Apr-2006 |
wenzelm <none@none> |
tuned;
|
#
3bf6e6b1 |
|
12-Apr-2006 |
wenzelm <none@none> |
moved print_theorems/theory to Isar/proof_display.ML;
|
#
8855a393 |
|
09-Apr-2006 |
wenzelm <none@none> |
Term.itselfT;
|
#
80d65d44 |
|
20-Mar-2006 |
wenzelm <none@none> |
avoid polymorphic equality;
|
#
054b0614 |
|
22-Feb-2006 |
wenzelm <none@none> |
simplified Pure conjunction, based on actual const;
|
#
be108470 |
|
15-Feb-2006 |
wenzelm <none@none> |
removed distinct, renamed gen_distinct to distinct;
|
#
d7c58a26 |
|
29-Jan-2006 |
wenzelm <none@none> |
proper order of trfuns;
|
#
fe6b97fd |
|
27-Jan-2006 |
wenzelm <none@none> |
moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);
|
#
1a99eec8 |
|
24-Jan-2006 |
wenzelm <none@none> |
export name_multi;
|
#
acdc5889 |
|
21-Jan-2006 |
wenzelm <none@none> |
simplified type attribute;
|
#
a12c0ed4 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory; added syntax (from Syntax/mixfix.ML); added HTML output syntax for _lambda;
|
#
e3517f6b |
|
14-Jan-2006 |
wenzelm <none@none> |
sane ERROR handling;
|
#
d43bfc3d |
|
12-Jan-2006 |
wenzelm <none@none> |
generic_setup: optional argument, defaults to Context.setup();
|
#
a03f8d52 |
|
07-Jan-2006 |
wenzelm <none@none> |
gen_names: preserve empty names;
|
#
d3b022c7 |
|
16-Dec-2005 |
haftmann <none@none> |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
#
d3e3a029 |
|
09-Dec-2005 |
haftmann <none@none> |
oriented result pairs in PureThy
|
#
be39cc14 |
|
06-Dec-2005 |
haftmann <none@none> |
re-oriented some result tuples in PureThy
|
#
39bc5f40 |
|
28-Oct-2005 |
wenzelm <none@none> |
datatype thmref: added Fact; renamed Goal constant to prop;
|
#
d1a35217 |
|
19-Oct-2005 |
wenzelm <none@none> |
added thm(s) retrieval functions (from goals.ML);
|
#
a943bc7d |
|
28-Sep-2005 |
wenzelm <none@none> |
Theory.add_finals_i;
|
#
347ce55a |
|
20-Sep-2005 |
haftmann <none@none> |
slight adaptions to library changes
|
#
62a67b20 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update; add_defs etc.: use Thm.get_axiom_i, which is independent from naming;
|
#
960204b0 |
|
13-Sep-2005 |
wenzelm <none@none> |
added generic_setup, add_oracle (from isar_thy.ML);
|
#
c968ef97 |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update;
|
#
fa28c3fe |
|
28-Aug-2005 |
wenzelm <none@none> |
export theorems_of;
|
#
1260ffb6 |
|
01-Aug-2005 |
wenzelm <none@none> |
Compress.init_data;
|
#
53bd14d2 |
|
13-Jul-2005 |
haftmann <none@none> |
(intermediate commit)
|
#
6fe107d0 |
|
06-Jul-2005 |
wenzelm <none@none> |
tuned forall_elim_var(s): avoid expensive Term.add_vars;
|
#
64dca2fd |
|
22-Jun-2005 |
wenzelm <none@none> |
renamed init to init_data;
|
#
8e2cf0ce |
|
21-Jun-2005 |
wenzelm <none@none> |
enter_thms: use theorem database of thy *after* attribute application;
|
#
22db87b1 |
|
20-Jun-2005 |
wenzelm <none@none> |
datatype thmref = Name ... | NameSelection ...; added print_theorems_diff; tuned;
|
#
e9383bb8 |
|
17-Jun-2005 |
wenzelm <none@none> |
added theorem_space; removed unused extern_thm_sg; accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; removed theory management (cf. 'history' in context.ML); moved add_typedecls to sign.ML; Sign.init, Theory.init; tuned;
|
#
1da84678 |
|
08-Jun-2005 |
wenzelm <none@none> |
thms_of no longer global; added all_thms_of; theorems: NameSpace.table;
|
#
7662be6a |
|
31-May-2005 |
wenzelm <none@none> |
renamed cond_extern to extern; removed note_thmss_accesses(_i) -- functionality covered by general naming context;
|
#
0d3b1a68 |
|
22-May-2005 |
wenzelm <none@none> |
added string_of_thmref, selections, fact_index_of, valid_thms; moved find_matching_thms, is_matching_thm, find_intros/intros_goal/elims to Isar/find_theorems.ML; tuned
|
#
56ad34ad |
|
17-May-2005 |
wenzelm <none@none> |
moved credit to CONTRIBUTORS;
|
#
64e465f6 |
|
16-May-2005 |
kleing <none@none> |
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
|
#
254b6c3e |
|
29-Apr-2005 |
kleing <none@none> |
credits
|
#
fbb4cc61 |
|
29-Apr-2005 |
kleing <none@none> |
new thms_containing that searches for patterns instead of constants (by Rafal Kolanski, NICTA)
|
#
9f1ea5d9 |
|
21-Apr-2005 |
wenzelm <none@none> |
superceded by Pure.thy and CPure.thy;
|
#
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.
|
#
b04389e3 |
|
13-Apr-2005 |
wenzelm <none@none> |
*** MESSAGE REFERS TO PREVIOUS VERSION *** added datatype interval, improved thm selections;
|
#
0f8c0167 |
|
13-Apr-2005 |
wenzelm <none@none> |
*** empty log message ***
|
#
50933e3d |
|
10-Apr-2005 |
ballarin <none@none> |
First release of interpretation commands.
|
#
44953e9d |
|
24-Mar-2005 |
ballarin <none@none> |
Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
d47d4b3b |
|
10-Feb-2005 |
berghofe <none@none> |
Fixed bug in select_thm.
|
#
82173bd6 |
|
10-Feb-2005 |
berghofe <none@none> |
Subscripts for theorem lists now start at 1.
|
#
8b1aab9e |
|
24-Jan-2005 |
berghofe <none@none> |
Specific theorems in a named list of theorems can now be referred to via indices (type thmref).
|
#
a6b54d14 |
|
08-Dec-2004 |
nipkow <none@none> |
fixed bug in find functions that I introduced some time ago.
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
4ca8e7a3 |
|
31-May-2004 |
wenzelm <none@none> |
removed obsolete sort 'logic';
|
#
e60eb0af |
|
26-Apr-2004 |
paulson <none@none> |
commented
|
#
bd1177ce |
|
14-Apr-2004 |
wenzelm <none@none> |
renamed have_thms to note_thms;
|
#
c2710455 |
|
11-Feb-2004 |
berghofe <none@none> |
Removed "duplicate fact binding" error message.
|
#
8c9b5354 |
|
09-Oct-2003 |
skalberg <none@none> |
Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
|
#
b66d7234 |
|
03-Feb-2003 |
berghofe <none@none> |
Moved find_intros_goal from goals.ML to pure_thy.ML
|
#
3365831f |
|
13-Nov-2002 |
berghofe <none@none> |
Fixed name clash problem in forall_elim_var.
|
#
e675a0aa |
|
21-Oct-2002 |
berghofe <none@none> |
Removed flexpair_def.
|
#
597e5ada |
|
14-Oct-2002 |
nipkow <none@none> |
Ported find_intro/elim to Isar.
|
#
06d95e5c |
|
27-Aug-2002 |
wenzelm <none@none> |
disallow duplicate fact bindings for drafts (i.e. within new-style theory files);
|
#
c6bcb55f |
|
26-Jul-2002 |
wenzelm <none@none> |
tuned;
|
#
38feff48 |
|
02-Jul-2002 |
wenzelm <none@none> |
improved thms_containing (use FactIndex.T etc.);
|
#
0fce208d |
|
07-Feb-2002 |
berghofe <none@none> |
Theorems are only "pre-named" if the do not already have names.
|
#
601f0d10 |
|
10-Jan-2002 |
wenzelm <none@none> |
have_thmss vs. have_thmss_i;
|
#
5b6eb766 |
|
09-Jan-2002 |
wenzelm <none@none> |
added hide_thms;
|
#
cadfdab8 |
|
27-Nov-2001 |
wenzelm <none@none> |
theory data: removed obsolete finish method;
|
#
134bbbf9 |
|
20-Nov-2001 |
wenzelm <none@none> |
trfuns *after* binder syntax;
|
#
18979ba8 |
|
19-Nov-2001 |
berghofe <none@none> |
Further restructuring of theorem naming functions.
|
#
feab7aa2 |
|
11-Nov-2001 |
wenzelm <none@none> |
renamed open_smart_store_thms to smart_store_thms_open; added Syntax.pure_syntax_output;
|
#
37c2ce11 |
|
08-Nov-2001 |
wenzelm <none@none> |
theory data: finish method;
|
#
c1499a97 |
|
31-Oct-2001 |
berghofe <none@none> |
- enter_thmx -> enter_thms - improved naming of theorems: enter_thms now takes functions pre_name and post_name as arguments
|
#
a62dda93 |
|
28-Sep-2001 |
wenzelm <none@none> |
internal thm numbering with ":" instead of "_";
|
#
2829cd89 |
|
31-Aug-2001 |
berghofe <none@none> |
Added equality axioms and initialization of proof term package.
|
#
d2fb7a2c |
|
13-Dec-2000 |
wenzelm <none@none> |
eliminated GOAL syntax;
|
#
21d58841 |
|
12-Nov-2000 |
wenzelm <none@none> |
Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
|
#
f31e97a5 |
|
17-Sep-2000 |
wenzelm <none@none> |
Display.pretty_thm_sg;
|
#
0ec279d6 |
|
02-Sep-2000 |
wenzelm <none@none> |
added get_thm_closure;
|
#
01426224 |
|
09-Aug-2000 |
wenzelm <none@none> |
added get_thms_closure, single_thm;
|
#
18218933 |
|
04-Aug-2000 |
wenzelm <none@none> |
dummy_pattern moved to term.ML;
|
#
6c9c1185 |
|
13-Jul-2000 |
wenzelm <none@none> |
add_defs(_i): overloaded option;
|
#
1b84fd86 |
|
03-Jul-2000 |
wenzelm <none@none> |
added "nothing" (empty list of theorems);
|
#
d0f3a9a3 |
|
01-Jul-2000 |
wenzelm <none@none> |
print_theorems: omit name space;
|
#
f875f788 |
|
29-Jun-2000 |
wenzelm <none@none> |
have_thmss: handle multiple lists of arguments;
|
#
b407e266 |
|
31-May-2000 |
wenzelm <none@none> |
get_thm(s): automatic transfer;
|
#
148d4e48 |
|
17-Apr-2000 |
wenzelm <none@none> |
Pretty.chunks;
|
#
df1382aa |
|
12-Mar-2000 |
wenzelm <none@none> |
add_thms, add_axioms, add_defs: return theorems as well;
|
#
df79c5df |
|
29-Nov-1999 |
wenzelm <none@none> |
Goal: tuned pris;
|
#
1152fb8a |
|
27-Oct-1999 |
wenzelm <none@none> |
dummy_pattern: aprop;
|
#
69147885 |
|
21-Oct-1999 |
wenzelm <none@none> |
forall_elim_var(s) move here from drule.ML; add_axioms/defs: forall_elim_vars on result;
|
#
2d70bced |
|
08-Oct-1999 |
wenzelm <none@none> |
theorem database now also indexes constants "Trueprop", "all", "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
|
#
10bdd2d0 |
|
06-Oct-1999 |
wenzelm <none@none> |
fixed naming of single axioms;
|
#
3c87bb5f |
|
06-Sep-1999 |
wenzelm <none@none> |
removed thms_closure (unused);
|
#
06623397 |
|
04-Sep-1999 |
wenzelm <none@none> |
eliminated default_name (thms no longer stored for name "");
|
#
1527f39c |
|
01-Sep-1999 |
wenzelm <none@none> |
smart_store_thms;
|
#
d483c74d |
|
18-Aug-1999 |
wenzelm <none@none> |
tuned Goal syntax;
|
#
a6935e9e |
|
12-Jul-1999 |
wenzelm <none@none> |
thms_containing: undeclared consts error;
|
#
61166137 |
|
28-Jun-1999 |
wenzelm <none@none> |
cond_extern_table;
|
#
e816c9e9 |
|
04-Jun-1999 |
wenzelm <none@none> |
fixed BUG in have_thmss: return thy';
|
#
4d5cdc5a |
|
21-May-1999 |
wenzelm <none@none> |
avoid string constants;
|
#
019e0913 |
|
21-May-1999 |
wenzelm <none@none> |
backup replaced by checkpoint;
|
#
bdb82697 |
|
17-May-1999 |
wenzelm <none@none> |
backup operation replaces transaction;
|
#
9d962912 |
|
04-May-1999 |
wenzelm <none@none> |
transaction: Theory.copy;
|
#
83f9293f |
|
30-Apr-1999 |
wenzelm <none@none> |
renamed 'dummy' to 'dummy_pattern' (less dangerous);
|
#
346fbb4a |
|
30-Apr-1999 |
wenzelm <none@none> |
theory data: copy; consts dummy :: 'a ("'_");
|
#
f68d2a48 |
|
17-Mar-1999 |
wenzelm <none@none> |
added cond_extern_thm_sg; have_thmss: name made optional;
|
#
8d9c85f3 |
|
11-Mar-1999 |
wenzelm <none@none> |
workaround default_name problem;
|
#
7f0251b2 |
|
12-Jan-1999 |
wenzelm <none@none> |
tuned signature;
|
#
d4846d64 |
|
12-Jan-1999 |
wenzelm <none@none> |
eliminated tthm type and Attribute structure;
|
#
5aca05a5 |
|
11-Dec-1998 |
oheimb <none@none> |
added new print_mode "xsymbols" for extended symbol support (e.g. genuiely long arrows)
|
#
a135a2a9 |
|
19-Nov-1998 |
wenzelm <none@none> |
no warning for "it" theorems;
|
#
7e73e0ed |
|
17-Nov-1998 |
wenzelm <none@none> |
added default_name; added have_tthmss;
|
#
487615e6 |
|
16-Nov-1998 |
wenzelm <none@none> |
Attribute.thms_of;
|
#
0905f5ee |
|
20-Oct-1998 |
wenzelm <none@none> |
Symtab.foldl;
|
#
8501a099 |
|
17-Aug-1998 |
wenzelm <none@none> |
added get_tthmss;
|
#
69fe640a |
|
06-Aug-1998 |
wenzelm <none@none> |
added store_tthm;
|
#
d638127a |
|
28-Jul-1998 |
wenzelm <none@none> |
removed global_names flag;
|
#
4a87c094 |
|
22-Jul-1998 |
wenzelm <none@none> |
moved long_names / cond_extern to name_space.ML;
|
#
d2177552 |
|
29-Jun-1998 |
wenzelm <none@none> |
tuned transaction; moved actual (C)Pure theories to pure.ML;
|
#
32f99294 |
|
17-Jun-1998 |
nipkow <none@none> |
Goals may now contain assumptions, which are not returned. This is controlled by an argument `atomic' to the goal commands.
|
#
c1e03fce |
|
10-Jun-1998 |
wenzelm <none@none> |
tuned transaction;
|
#
6509846b |
|
10-Jun-1998 |
wenzelm <none@none> |
moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;
|
#
1b524386 |
|
08-Jun-1998 |
wenzelm <none@none> |
use type-safe theory data interface;
|
#
c29479e1 |
|
05-Jun-1998 |
wenzelm <none@none> |
added print_theorems: theory -> unit; added print_theory: theory -> unit; added transaction mechanism as last resort to accomodate non-atomic transformers (please avoid such things); tuned setup;
|
#
7bd7bbae |
|
25-May-1998 |
wenzelm <none@none> |
added get_name, put_name, global_path, local_path, begin_theory, end_theory;
|
#
ab0f746d |
|
15-May-1998 |
wenzelm <none@none> |
added add_axioms_x, add_defs_x;
|
#
05714ffb |
|
12-May-1998 |
wenzelm <none@none> |
added thms_closure: theory -> xstring -> tthm list option; added add_typedecls: (bstring * string list * mixfix) list -> theory -> theory; |> Theory.add_nonterminals Syntax.pure_nonterms;
|
#
fa2b2a4b |
|
29-Apr-1998 |
wenzelm <none@none> |
tuned names of (add_)store_XXX functions; added attributes to add_thms, add_axioms, add_defs functions;
|
#
870997ac |
|
03-Apr-1998 |
wenzelm <none@none> |
type_error;
|
#
55118eed |
|
04-Apr-1998 |
wenzelm <none@none> |
added Goal_def;
|
#
f713fe11 |
|
03-Apr-1998 |
wenzelm <none@none> |
added get_tthm(s), store_tthms(s); tuned;
|
#
3842fb6f |
|
30-Jan-1998 |
wenzelm <none@none> |
tuned msgs;
|
#
e4413f61 |
|
29-Dec-1997 |
wenzelm <none@none> |
pretty_name_space;
|
#
433bbc56 |
|
28-Dec-1997 |
wenzelm <none@none> |
renamed Symtab.null to Symtab.empty;
|
#
d7d715f8 |
|
20-Nov-1997 |
wenzelm <none@none> |
improved theorems print method: transfer_sg;
|
#
0a8c6f5b |
|
04-Nov-1997 |
wenzelm <none@none> |
type object = exn (enhance readability);
|
#
2947e11f |
|
03-Nov-1997 |
wenzelm <none@none> |
made SML/97 happy;
|
#
c71c8ab7 |
|
30-Oct-1997 |
wenzelm <none@none> |
tuned thy_data;
|
#
77f6b932 |
|
30-Oct-1997 |
wenzelm <none@none> |
tuned;
|
#
9fd16fe8 |
|
28-Oct-1997 |
wenzelm <none@none> |
added ignored_consts, thms_containing, add_store_axioms(_i), add_store_defs(_i), thms_of; tuned pure thys;
|
#
b14c4b44 |
|
27-Oct-1997 |
wenzelm <none@none> |
oops;
|
#
fde4c303 |
|
27-Oct-1997 |
wenzelm <none@none> |
renamed put_* to store_*;
|
#
78a0a04a |
|
24-Oct-1997 |
wenzelm <none@none> |
oops, swap warnings;
|
#
aba74ea2 |
|
24-Oct-1997 |
wenzelm <none@none> |
Init 'theorems' data. The Pure theories.
|