| 2002-07-02 |
wenzelm |
2002-07-02 |
thms_containing: optional limit argument;
|
file | diff | annotate |
| 2002-07-02 |
wenzelm |
2002-07-02 |
* improved thms_containing: proper indexing of facts instead of raw
theorems; check validity of results wrt. current name space; include
local facts of proof configuration (also covers active locales);
|
file | diff | annotate |
| 2002-05-31 |
nipkow |
2002-05-31 |
*** empty log message ***
|
file | diff | annotate |
| 2002-05-30 |
nipkow |
2002-05-30 |
*** empty log message ***
|
file | diff | annotate |
| 2002-05-17 |
nipkow |
2002-05-17 |
*** empty log message ***
|
file | diff | annotate |
| 2002-03-07 |
wenzelm |
2002-03-07 |
tuned;
|
file | diff | annotate |
| 2002-03-05 |
wenzelm |
2002-03-05 |
tuned;
|
file | diff | annotate |
| 2002-03-05 |
berghofe |
2002-03-05 |
Added two paragraphs on "rules" method and code generator.
|
file | diff | annotate |
| 2002-02-28 |
wenzelm |
2002-02-28 |
fixed date;
|
file | diff | annotate |
| 2002-02-27 |
wenzelm |
2002-02-27 |
tuned;
|
file | diff | annotate |
| 2002-02-21 |
wenzelm |
2002-02-21 |
* HOL: removed obsolete theorem "optionE";
|
file | diff | annotate |
| 2002-02-21 |
wenzelm |
2002-02-21 |
* HOL: removed obsolete theorem "optionE";
|
file | diff | annotate |
| 2002-02-19 |
wenzelm |
2002-02-19 |
"isatool usedir -D output HOL Test && isatool document Test/output";
|
file | diff | annotate |
| 2002-02-14 |
nipkow |
2002-02-14 |
*** empty log message ***
|
file | diff | annotate |
| 2002-02-12 |
wenzelm |
2002-02-12 |
* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
|
file | diff | annotate |
| 2002-01-26 |
wenzelm |
2002-01-26 |
Isar cases/induct: no backtracking;
|
file | diff | annotate |
| 2002-01-25 |
paulson |
2002-01-25 |
ZF
|
file | diff | annotate |
| 2002-01-23 |
wenzelm |
2002-01-23 |
* HOL: nat_number_of;
|
file | diff | annotate |
| 2002-01-21 |
wenzelm |
2002-01-21 |
* Pure/show_hyps reset by default (in accordance to existing Isar practice);
|
file | diff | annotate |
| 2002-01-16 |
paulson |
2002-01-16 |
Isar version of ZF/AC
|
file | diff | annotate |
| 2002-01-15 |
wenzelm |
2002-01-15 |
tuned;
|
file | diff | annotate |
| 2002-01-15 |
wenzelm |
2002-01-15 |
Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
|
file | diff | annotate |
| 2002-01-14 |
wenzelm |
2002-01-14 |
* system: reduced base memory usage by Poly/ML (approx. 20 MB instead
of 40 MB), cf. ML_OPTIONS;
|
file | diff | annotate |
| 2002-01-13 |
wenzelm |
2002-01-13 |
* HOL: symbolic syntax for x^2 (numeral 2);
|
file | diff | annotate |
| 2002-01-13 |
wenzelm |
2002-01-13 |
HOL-Real/Complex_Numbers;
|
file | diff | annotate |
| 2002-01-12 |
wenzelm |
2002-01-12 |
tuned;
|
file | diff | annotate |
| 2002-01-11 |
wenzelm |
2002-01-11 |
Isabelle2002 (January 2002);
|
file | diff | annotate |
| 2002-01-11 |
wenzelm |
2002-01-11 |
* Pure: localized 'lemmas', 'theorems', 'declare';
|
file | diff | annotate |
| 2002-01-09 |
wenzelm |
2002-01-09 |
* added \<euro> symbol;
* HOL-Hyperreal is now a logic image;
* isatool latex no longer depends on changed TEXINPUTS;
|
file | diff | annotate |
| 2002-01-03 |
wenzelm |
2002-01-03 |
tuned;
|
file | diff | annotate |
| 2001-12-29 |
wenzelm |
2001-12-29 |
* ZF/IMP: updated and converted to new-style theory format;
|
file | diff | annotate |
| 2001-12-27 |
wenzelm |
2001-12-27 |
HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
|
file | diff | annotate |
| 2001-12-21 |
wenzelm |
2001-12-21 |
HOL/record: shared operations ("more", "fields", etc.) now need to be
always qualified;
|
file | diff | annotate |
| 2001-12-20 |
nipkow |
2001-12-20 |
*** empty log message ***
|
file | diff | annotate |
| 2001-12-20 |
paulson |
2001-12-20 |
ZF/Main
|
file | diff | annotate |
| 2001-12-18 |
wenzelm |
2001-12-18 |
* system: tested support for MacOS X;
|
file | diff | annotate |
| 2001-12-13 |
nipkow |
2001-12-13 |
*** empty log message ***
|
file | diff | annotate |
| 2001-12-11 |
wenzelm |
2001-12-11 |
tuned;
|
file | diff | annotate |
| 2001-12-11 |
wenzelm |
2001-12-11 |
isatools "symbolinput" and "nonascii" have disappeared;
|
file | diff | annotate |
| 2001-12-10 |
wenzelm |
2001-12-10 |
* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
of "lam" -- INCOMPATIBILITY;
|
file | diff | annotate |
| 2001-12-06 |
wenzelm |
2001-12-06 |
* Pure/obtain: "thesis" now internal (use ?thesis);
* Pure: generic 'sym' / 'symmetric' attributes;
* Provers/classical: 'swapped' attribute;
* HOL: proper rules less_induct and wf_induct_rule;
|
file | diff | annotate |
| 2001-12-05 |
wenzelm |
2001-12-05 |
* Pure/Provers/classical: simplified integration with pure rule
attributes and methods;
|
file | diff | annotate |
| 2001-12-01 |
wenzelm |
2001-12-01 |
* HOL: the class of all HOL types is now called "type" rather than
"term"; INCOMPATIBILITY, need to adapt references to this type class
in axclass/classes, instance/arities, and (usually rare) occurrences
in typings (of consts etc.); internally the class is called
"HOL.type", ML programs should refer to HOLogic.typeS;
|
file | diff | annotate |
| 2001-11-28 |
wenzelm |
2001-11-28 |
* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode;
* Pure/syntax: "x::_::foo" sort constraints;
|
file | diff | annotate |
| 2001-11-24 |
wenzelm |
2001-11-24 |
tuned;
|
file | diff | annotate |
| 2001-11-20 |
wenzelm |
2001-11-20 |
* HOL/record: cases/induct for more parts;
* syntax: prefer later print_translation functions;
|
file | diff | annotate |
| 2001-11-20 |
paulson |
2001-11-20 |
Hyperreal
|
file | diff | annotate |
| 2001-11-15 |
wenzelm |
2001-11-15 |
* ZF: new-style theory commands '(co)inductive', '(co)datatype',
'rep_datatype', 'inductive_cases'; also methods 'ind_cases',
'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
|
file | diff | annotate |
| 2001-11-13 |
wenzelm |
2001-11-13 |
* ZF: new-style theory commands 'inductive', 'inductive_cases', and
methods 'ind_cases', 'induct_tac', 'case_tac';
|
file | diff | annotate |
| 2001-11-12 |
wenzelm |
2001-11-12 |
Isar: 'induct' proper support for mutual induction involving
non-atomic rule statements;
Isar/Pure: support multiple simultaneous goal statements;
|
file | diff | annotate |
| 2001-11-12 |
paulson |
2001-11-12 |
ZF/Induct,UNITY
|
file | diff | annotate |
| 2001-11-08 |
wenzelm |
2001-11-08 |
* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac,
etc.) now consider the syntactic context of assumptions, giving a
better chance to get type-inference of the arguments right (this is
especially important for locales);
* system: refrain from any attempt at filtering input streams; no
longer support ``8bit'' encoding of old isabelle font, instead proper
iso-latin characters may now be used;
|
file | diff | annotate |
| 2001-11-06 |
wenzelm |
2001-11-06 |
* Isar/Pure: proper integration with ``locales''; unlike the original
version by Florian Kammueller, Isar locales package high-level proof
contexts rather than raw logical ones (e.g. we admit to include
attributes everywhere);
* Isar/Pure: theory goals now support ad-hoc contexts, which are
discharged in the result, as in ``lemma (assumes A and B) K: A .'';
syntax coincides with that of a locale body;
|
file | diff | annotate |
| 2001-11-03 |
wenzelm |
2001-11-03 |
* 'domain' package adapted to new-style theories, e.g. see
HOLCF/ex/Dnat.thy;
|
file | diff | annotate |
| 2001-11-03 |
wenzelm |
2001-11-03 |
HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
instead of lift.induct_tac, use UU instead of Undef in cases;
|
file | diff | annotate |
| 2001-10-31 |
wenzelm |
2001-10-31 |
- 'induct' may now use elim-style induction rules without chaining
facts, using ``missing'' premises from the goal state; this allows
rules stemming from inductive sets to be applied in unstructured
scripts, while still benefitting from proper handling of non-atomic
statements; NB: major inductive premises need to be put first, all the
rest of the goal is passed through the induction;
|
file | diff | annotate |
| 2001-10-30 |
wenzelm |
2001-10-30 |
- 'induct' method now derives symbolic cases from the *rulified* rule
(before it used to rulify cases stemming from the internal atomized
version); this means that the context of a non-atomic statement
becomes is included in the hypothesis, avoiding the slightly
cumbersome show "PROP ?case" form;
|
file | diff | annotate |
| 2001-10-27 |
wenzelm |
2001-10-27 |
* Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;
|
file | diff | annotate |
| 2001-10-26 |
wenzelm |
2001-10-26 |
* Pure: method 'atomize' presents local goal premises as object-level
statements (atomic meta-level propositions); setup controlled via
rewrite rules declarations of 'atomize' attribute; example
application: 'induct' method with proper rule statements in improper
proof *scripts*;
|
file | diff | annotate |
| 2001-10-25 |
wenzelm |
2001-10-25 |
* HOL/record:
- removed "more" class (simply use "term") -- INCOMPATIBILITY;
|
file | diff | annotate |