| 2019-01-05 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| 2016-06-23 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2016-05-30 |
wenzelm |
allow 'for' fixes for multi_specs;
|
file |
diff |
annotate
|
| 2016-04-28 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| 2015-04-10 |
blanchet |
renamed ML funs
|
file |
diff |
annotate
|
| 2015-04-06 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|
| 2015-04-06 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| 2015-03-27 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2015-03-24 |
wenzelm |
clarified case_tac fixes and context;
|
file |
diff |
annotate
|
| 2015-02-10 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| 2014-09-17 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
file |
diff |
annotate
|
| 2014-09-11 |
blanchet |
speed up old Nominal by killing type variables
|
file |
diff |
annotate
|
| 2014-09-08 |
blanchet |
ported old Nominal to use new datatypes
|
file |
diff |
annotate
|
| 2014-09-08 |
blanchet |
use compatibility layer
|
file |
diff |
annotate
|
| 2014-09-01 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| 2014-09-01 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
| 2014-03-22 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| 2013-12-14 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| 2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| 2013-04-10 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| 2013-04-10 |
wenzelm |
formal proof context for axclass proofs;
|
file |
diff |
annotate
|
| 2012-03-16 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| 2012-01-10 |
berghofe |
Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete
|
file |
diff |
annotate
|
| 2011-12-24 |
haftmann |
treatment of type constructor `set`
|
file |
diff |
annotate
|
| 2011-12-13 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| 2011-11-30 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
| 2011-10-12 |
wenzelm |
modernized structure Induct_Tacs;
|
file |
diff |
annotate
|
| 2011-09-03 |
haftmann |
tuned specifications
|
file |
diff |
annotate
|
| 2011-09-03 |
haftmann |
assert Pure equations for theorem references; tuned
|
file |
diff |
annotate
|
| 2011-01-15 |
berghofe |
Finally removed old primrec package, since Primrec.add_primrec_global
|
file |
diff |
annotate
|
| 2010-12-15 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| 2010-09-20 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| 2010-07-01 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| 2010-06-10 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| 2010-05-17 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| 2009-11-08 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| 2009-10-17 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| 2009-10-15 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| 2009-06-23 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| 2009-06-23 |
haftmann |
add_datatypes does not yield particular rules any longer
|
file |
diff |
annotate
|
| 2009-06-23 |
haftmann |
add_datatype interface yields type names and less rules
|
file |
diff |
annotate
|
| 2009-06-21 |
haftmann |
simplified names of common datatype types
|
file |
diff |
annotate
|
| 2009-06-19 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| 2009-06-17 |
haftmann |
datatype packages: record datatype_config for configuration flags; less verbose signatures
|
file |
diff |
annotate
|
| 2009-05-07 |
haftmann |
explicit type_name antiquotations
|
file |
diff |
annotate
|
| 2009-03-19 |
wenzelm |
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
|
file |
diff |
annotate
|
| 2009-03-07 |
wenzelm |
more uniform handling of binding in packages;
|
file |
diff |
annotate
|
| 2009-03-04 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| 2009-02-25 |
berghofe |
Added equivariance lemmas for fresh_star.
|
file |
diff |
annotate
|
| 2009-01-21 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| 2008-12-16 |
Christian Urban |
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
|
file |
diff |
annotate
|
| 2008-12-04 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| 2008-11-10 |
berghofe |
Some more functions for accessing information about atoms.
|
file |
diff |
annotate
|
| 2008-09-26 |
berghofe |
Added some more theorems to NominalData.
|
file |
diff |
annotate
|
| 2008-09-02 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| 2008-08-27 |
urbanc |
added equivariance lemmas for ex1 and the
|
file |
diff |
annotate
|
| 2008-07-29 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| 2008-06-30 |
urbanc |
added facts to lemma swap_simps and tuned lemma calc_atms
|
file |
diff |
annotate
|
| 2008-06-14 |
wenzelm |
InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
|
file |
diff |
annotate
|