#
ce285df7 |
|
06-Mar-2018 |
ballarin <none@none> |
Drop rewrite rule arguments of sublocale and interpretation implementations.
|
#
fa96ec06 |
|
16-Jan-2018 |
ballarin <none@none> |
Experimental support for rewrite morphisms in locale instances.
|
#
f59d9068 |
|
04-Aug-2017 |
haftmann <none@none> |
provide explicit variant initializers for regular named target vs. almost-named target
|
#
0293ac2c |
|
06-Jul-2016 |
wenzelm <none@none> |
tuned signature;
|
#
5dc803d8 |
|
13-Apr-2016 |
wenzelm <none@none> |
eliminated "xname" and variants;
|
#
81b459a5 |
|
08-Apr-2016 |
wenzelm <none@none> |
eliminated unused simproc identifier;
|
#
1937e988 |
|
14-Nov-2015 |
haftmann <none@none> |
represent both algebraic and local-theory views on locale interpretation in interfaces --HG-- extra : rebase_source : 0f233aa5dd88ebb1594d03af4f3a3d7b08a44fa7
|
#
d7bdc08d |
|
14-Nov-2015 |
haftmann <none@none> |
separate ML module for interpretation --HG-- extra : rebase_source : 867de135491ddc9e949d932384cce64f60343123
|
#
104f7005 |
|
09-Nov-2015 |
wenzelm <none@none> |
uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;
|
#
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
#
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
#
b8ef3466 |
|
01-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
#
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
#
45a2f5f8 |
|
01-Apr-2015 |
wenzelm <none@none> |
imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
40b52875 |
|
06-Jun-2014 |
haftmann <none@none> |
dropped obscure and unused ad-hoc before_exit hook for named targets
|
#
1a2798f1 |
|
07-Mar-2014 |
wenzelm <none@none> |
removed dead code;
|
#
34f8a28f |
|
23-Apr-2013 |
haftmann <none@none> |
target-sensitive user-level commands interpretation and sublocale
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
55014c61 |
|
26-Nov-2012 |
wenzelm <none@none> |
tuned command descriptions;
|
#
607fed84 |
|
17-Oct-2012 |
wenzelm <none@none> |
more method position information, notably finished_pos after end of previous text;
|
#
c9f94e8d |
|
16-Oct-2012 |
wenzelm <none@none> |
more proof method text position information;
|
#
552f54ad |
|
10-Oct-2012 |
wenzelm <none@none> |
more explicit namespace prefix for 'statespace' -- duplicate facts;
|
#
3b1dbbe5 |
|
08-Aug-2012 |
wenzelm <none@none> |
tuned signature;
|
#
150d8520 |
|
16-Mar-2012 |
wenzelm <none@none> |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
#
de9fb383 |
|
15-Mar-2012 |
wenzelm <none@none> |
prefer formally checked @{keyword} parser;
|
#
97cdd6ec |
|
14-Mar-2012 |
wenzelm <none@none> |
locale expressions without source positions;
|
#
c15e8515 |
|
02-Dec-2011 |
wenzelm <none@none> |
eliminated some legacy operations;
|
#
ac946949 |
|
28-Nov-2011 |
wenzelm <none@none> |
tuned messages;
|
#
00eaa897 |
|
06-Nov-2011 |
wenzelm <none@none> |
misc tuning and modernization; more antiquotations;
|
#
65bd1be2 |
|
06-Nov-2011 |
wenzelm <none@none> |
tuned;
|
#
01244fea |
|
28-Oct-2011 |
wenzelm <none@none> |
uniform Local_Theory.declaration with explicit params;
|
#
68ed89ae |
|
10-Aug-2011 |
wenzelm <none@none> |
old term operations are legacy;
|
#
9c72c6e0 |
|
29-Jun-2011 |
wenzelm <none@none> |
simplified/unified Simplifier.mk_solver;
|
#
ec1196d6 |
|
09-Jun-2011 |
wenzelm <none@none> |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
#
390ebc4a |
|
08-Jun-2011 |
wenzelm <none@none> |
more robust exception pattern General.Subscript;
|
#
f176da4e |
|
27-Apr-2011 |
wenzelm <none@none> |
reorganized fixes as specialized (global) name space;
|
#
7cfe82ef |
|
16-Apr-2011 |
wenzelm <none@none> |
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;
|
#
d1a2ff7b |
|
16-Apr-2011 |
wenzelm <none@none> |
eliminated old List.nth; tuned;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
a4d04f8b |
|
08-Apr-2011 |
wenzelm <none@none> |
discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
|
#
3aaf94cf |
|
06-Apr-2011 |
wenzelm <none@none> |
separate structure Term_Position; dismantled remains of structure Type_Ext;
|
#
a67f4598 |
|
22-Mar-2011 |
wenzelm <none@none> |
statespace syntax: strip positions -- type constraints are unexpected here;
|
#
3208ca68 |
|
16-Jan-2011 |
wenzelm <none@none> |
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
|
#
ef2d6500 |
|
08-Jan-2011 |
wenzelm <none@none> |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
#
c2e1cf8b |
|
18-Dec-2010 |
ballarin <none@none> |
Add mixins to sublocale command.
|
#
d19dab54 |
|
05-Sep-2010 |
wenzelm <none@none> |
turned show_sorts/show_types into proper configuration options;
|
#
b11705e1 |
|
28-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix equality now named HOL.eq
|
#
b2baf2b0 |
|
27-Aug-2010 |
wenzelm <none@none> |
eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; modernized attribute setup;
|
#
2ab2e08e |
|
25-Aug-2010 |
wenzelm <none@none> |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
#
33076e76 |
|
19-Aug-2010 |
haftmann <none@none> |
tuned quotes
|
#
bbda5041 |
|
19-Aug-2010 |
haftmann <none@none> |
use antiquotations for remaining unqualified constants in HOL
|
#
be4c7e28 |
|
12-Aug-2010 |
haftmann <none@none> |
Named_Target.init: empty string represents theory target
|
#
2fa88f89 |
|
11-Aug-2010 |
haftmann <none@none> |
renamed Theory_Target to the more appropriate Named_Target --HG-- rename : src/Pure/Isar/theory_target.ML => src/Pure/Isar/named_target.ML
|
#
5a9d2980 |
|
27-May-2010 |
wenzelm <none@none> |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
#
7a6b0131 |
|
17-May-2010 |
wenzelm <none@none> |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
|
#
933b3352 |
|
17-May-2010 |
wenzelm <none@none> |
tuned;
|
#
4549e8d1 |
|
05-May-2010 |
haftmann <none@none> |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
#
60d6d298 |
|
03-May-2010 |
wenzelm <none@none> |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
#
27935f48 |
|
29-Apr-2010 |
wenzelm <none@none> |
adapted ProofContext.infer_type;
|
#
83628799 |
|
15-Apr-2010 |
wenzelm <none@none> |
inline old Record.read_typ/cert_typ; spelling;
|
#
d28e2372 |
|
13-Nov-2009 |
wenzelm <none@none> |
modernized structure Local_Theory;
|
#
8ce10e6a |
|
10-Nov-2009 |
wenzelm <none@none> |
modernized structure Theory_Target;
|
#
dfa769e1 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Generic_Data, Proof_Data; tuned;
|
#
296c7062 |
|
05-Nov-2009 |
wenzelm <none@none> |
adapted LocalTheory.declaration;
|
#
ec3bd0dd |
|
27-Oct-2009 |
wenzelm <none@none> |
critical comments;
|
#
b2816004 |
|
17-Oct-2009 |
wenzelm <none@none> |
indicate CRITICAL nature of various setmp combinators;
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
75401f7b |
|
15-Oct-2009 |
wenzelm <none@none> |
replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
|
#
0d8b21de |
|
23-Sep-2009 |
hoelzl <none@none> |
Undo errornous commit of Statespace change
|
#
b24bc37d |
|
23-Sep-2009 |
hoelzl <none@none> |
correct variable order in approximate-method
|
#
dbb847ed |
|
28-Aug-2009 |
wenzelm <none@none> |
modernized messages -- eliminated ctyp/cterm operations;
|
#
5371dea8 |
|
25-Jul-2009 |
wenzelm <none@none> |
Method.Basic: no position;
|
#
91b337ca |
|
19-Jun-2009 |
haftmann <none@none> |
discontinued ancient tradition to suffix certain ML module names with "_package" --HG-- rename : src/HOL/Import/import_package.ML => src/HOL/Import/import.ML rename : src/HOL/Nominal/nominal_package.ML => src/HOL/Nominal/nominal.ML rename : src/HOL/Tools/specification_package.ML => src/HOL/Tools/choice_specification.ML rename : src/HOL/Tools/datatype_package/datatype_package.ML => src/HOL/Tools/datatype_package/datatype.ML rename : src/HOL/Tools/function_package/fundef_package.ML => src/HOL/Tools/function_package/fundef.ML rename : src/HOL/Tools/inductive_package.ML => src/HOL/Tools/inductive.ML rename : src/HOL/Tools/inductive_set_package.ML => src/HOL/Tools/inductive_set.ML rename : src/HOL/Tools/old_primrec_package.ML => src/HOL/Tools/old_primrec.ML rename : src/HOL/Tools/primrec_package.ML => src/HOL/Tools/primrec.ML rename : src/HOL/Tools/recdef_package.ML => src/HOL/Tools/recdef.ML rename : src/HOL/Tools/record_package.ML => src/HOL/Tools/record.ML rename : src/HOL/Tools/typecopy_package.ML => src/HOL/Tools/typecopy.ML rename : src/HOL/Tools/typedef_package.ML => src/HOL/Tools/typedef.ML
|
#
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
#
ee2e7b78 |
|
12-Mar-2009 |
wenzelm <none@none> |
Assumption.all_prems_of, Assumption.all_assms_of;
|
#
b1ef46dc |
|
08-Mar-2009 |
wenzelm <none@none> |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
#
16aa5527 |
|
07-Mar-2009 |
wenzelm <none@none> |
minimal adaptions for abstract binding type;
|
#
da1c433c |
|
05-Mar-2009 |
wenzelm <none@none> |
removed spurious occurrences of old rep_ss;
|
#
e3913b9b |
|
04-Mar-2009 |
wenzelm <none@none> |
renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
|
#
a80e4f59 |
|
04-Mar-2009 |
haftmann <none@none> |
less arbitrary occurrences of undefined
|
#
c404586d |
|
07-Jan-2009 |
haftmann <none@none> |
changed locale predicate name convention
|
#
0e10d319 |
|
06-Jan-2009 |
haftmann <none@none> |
locale -> old_locale, new_locale -> locale
|
#
9a32058c |
|
05-Jan-2009 |
haftmann <none@none> |
locale -> old_locale, new_locale -> locale --HG-- rename : src/Pure/Isar/locale.ML => src/Pure/Isar/old_locale.ML
|
#
46b66c09 |
|
01-Jan-2009 |
wenzelm <none@none> |
avoid implicit use of prems;
|
#
4d527bca |
|
18-Dec-2008 |
Norbert Schirmer <norbert.schirmer@web.de> |
adapted statespace module to new locales;
|
#
b91805aa |
|
10-Dec-2008 |
wenzelm <none@none> |
more antiquotations;
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
3a3b3618 |
|
17-Nov-2008 |
haftmann <none@none> |
adjusted locale signature to *_cmd convention
|
#
5dbe4f0d |
|
29-Sep-2008 |
wenzelm <none@none> |
LocalTheory.exit_global;
|
#
d5fd3887 |
|
22-Sep-2008 |
haftmann <none@none> |
fixed headers
|
#
f31abf48 |
|
02-Sep-2008 |
wenzelm <none@none> |
explicit type Name.binding for higher-specification elements;
|
#
ef619048 |
|
24-Jul-2008 |
haftmann <none@none> |
dropped locale (open)
|
#
beabe47b |
|
19-Jun-2008 |
wenzelm <none@none> |
tuned signature; removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);
|
#
2173cb24 |
|
19-Jun-2008 |
wenzelm <none@none> |
tuned signature; removed duplicate of RecordPackage.read_typ; replaced Typetab by existing Typtab;
|
#
1a1b9232 |
|
29-Mar-2008 |
wenzelm <none@none> |
purely functional setup of claset/simpset/clasimpset;
|
#
1d75429e |
|
29-Mar-2008 |
wenzelm <none@none> |
eliminated quiete_mode ref (not really needed);
|
#
a6513468 |
|
19-Mar-2008 |
wenzelm <none@none> |
simplified get_thm(s): back to plain name argument;
|
#
a46b31e4 |
|
19-Mar-2008 |
wenzelm <none@none> |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
#
6ffa84a1 |
|
28-Jan-2008 |
wenzelm <none@none> |
added ::: / @@@ scanner combinators;
|
#
982ae1f0 |
|
18-Dec-2007 |
wenzelm <none@none> |
PrintMode.setmp (avoid direct access to print_mode ref);
|
#
1fc22904 |
|
12-Nov-2007 |
schirmer <none@none> |
added signatures; tuned
|
#
d93a6fb8 |
|
24-Oct-2007 |
schirmer <none@none> |
added Statespace library
|