| 2000-08-17 |
wenzelm |
Isar/Pure: renamed 'RS' attribute to 'THEN';
|
file |
diff |
annotate
|
| 2000-08-11 |
paulson |
ZF arith
|
file |
diff |
annotate
|
| 2000-08-07 |
paulson |
ZF arith
|
file |
diff |
annotate
|
| 2000-08-01 |
wenzelm |
* blast(_tac) now handles actual object-logic rules as assumptions;
|
file |
diff |
annotate
|
| 2000-07-28 |
nipkow |
* HOL/While
|
file |
diff |
annotate
|
| 2000-07-24 |
wenzelm |
* Isar/Provers: intro/elim/dest attributes: changed
|
file |
diff |
annotate
|
| 2000-07-21 |
oheimb |
strengthened force_tac by using new first_best_tac
|
file |
diff |
annotate
|
| 2000-07-19 |
paulson |
// change; also moved entry for AddIffs
|
file |
diff |
annotate
|
| 2000-07-18 |
wenzelm |
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
|
file |
diff |
annotate
|
| 2000-07-16 |
wenzelm |
* tuned AST representation of nested pairs, avoiding bogus output in
|
file |
diff |
annotate
|
| 2000-07-14 |
paulson |
AddIffs
|
file |
diff |
annotate
|
| 2000-07-13 |
wenzelm |
HOL: the disjoint sum is now "<+>" instead of "Plus";
|
file |
diff |
annotate
|
| 2000-07-12 |
wenzelm |
infix 'OF' is a version of 'MRS' with more appropriate argument order;
|
file |
diff |
annotate
|
| 2000-07-03 |
wenzelm |
* added 'nothing' --- the empty list of theorems;
|
file |
diff |
annotate
|
| 2000-07-01 |
wenzelm |
* Isar/HOL/Calculation: new rules for substitution in inequalities
|
file |
diff |
annotate
|
| 2000-07-01 |
wenzelm |
* Isar: removed 'help' command, which hasn't been too helpful anyway;
|
file |
diff |
annotate
|
| 2000-06-29 |
wenzelm |
* formal comments (text blocks etc.) in new-style theories may now
|
file |
diff |
annotate
|
| 2000-06-29 |
paulson |
weak elimination rules
|
file |
diff |
annotate
|
| 2000-06-16 |
paulson |
real simprocs
|
file |
diff |
annotate
|
| 2000-06-09 |
wenzelm |
* browser info session directories are now self-contained (may be put
|
file |
diff |
annotate
|
| 2000-06-07 |
wenzelm |
provide TAGS file for Isabelle sources;
|
file |
diff |
annotate
|
| 2000-06-02 |
oheimb |
added HOL/Prolog
|
file |
diff |
annotate
|
| 2000-05-31 |
wenzelm |
Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to
|
file |
diff |
annotate
|
| 2000-05-30 |
wenzelm |
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
|
file |
diff |
annotate
|
| 2000-05-28 |
wenzelm |
case 'antecedent';
|
file |
diff |
annotate
|
| 2000-05-25 |
paulson |
overloading of 0
|
file |
diff |
annotate
|
| 2000-05-23 |
nipkow |
SetInterval
|
file |
diff |
annotate
|
| 2000-05-22 |
wenzelm |
* Pure: changed syntax of local blocks from {{ }} to { };
|
file |
diff |
annotate
|
| 2000-05-18 |
wenzelm |
* HOL/ML: even fewer consts are declared as global (see theories Ord,
|
file |
diff |
annotate
|
| 2000-05-09 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2000-05-08 |
paulson |
more details
|
file |
diff |
annotate
|
| 2000-05-04 |
paulson |
simprocs
|
file |
diff |
annotate
|
| 2000-04-18 |
paulson |
new simprocs for numerals of type "nat"
|
file |
diff |
annotate
|
| 2000-04-17 |
wenzelm |
* improved name spaces: ambiguous output is qualified; support for
|
file |
diff |
annotate
|
| 2000-04-13 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-04-05 |
wenzelm |
Isar: simplified (more robust) goal selection of proof methods;
|
file |
diff |
annotate
|
| 2000-04-01 |
wenzelm |
recdef: admit name and atts;
|
file |
diff |
annotate
|
| 2000-03-30 |
nipkow |
recdef
|
file |
diff |
annotate
|
| 2000-03-30 |
wenzelm |
* Isar/Pure: local results and corresponding term bindings are now
|
file |
diff |
annotate
|
| 2000-03-29 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-03-24 |
wenzelm |
HOL/ex/Multiquote;
|
file |
diff |
annotate
|
| 2000-03-24 |
wenzelm |
usedir -D: update styles;
|
file |
diff |
annotate
|
| 2000-03-20 |
wenzelm |
improved support for emulating tactic scripts;
|
file |
diff |
annotate
|
| 2000-03-18 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2000-03-15 |
wenzelm |
Isar: splitter support; improved diagnostics;
|
file |
diff |
annotate
|
| 2000-03-13 |
wenzelm |
* HOL: exhaust_tac on datatypes superceded by new case_tac;
|
file |
diff |
annotate
|
| 2000-03-13 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2000-03-10 |
nipkow |
cases_tac
|
file |
diff |
annotate
|
| 2000-03-09 |
paulson |
Factorization
|
file |
diff |
annotate
|
| 2000-03-08 |
wenzelm |
* isatool mkdir provides easy setup of Isabelle session directories,
|
file |
diff |
annotate
|
| 2000-02-22 |
wenzelm |
* Pure now provides its own version of intro/elim/dest attributes;
|
file |
diff |
annotate
|
| 2000-02-21 |
wenzelm |
HOL/record: fixed select-update simplification procedure to handle
|
file |
diff |
annotate
|
| 2000-02-07 |
wenzelm |
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
|
file |
diff |
annotate
|
| 2000-02-02 |
wenzelm |
nat as names;
|
file |
diff |
annotate
|
| 1999-11-12 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-11-11 |
paulson |
HOL changes
|
file |
diff |
annotate
|
| 1999-11-11 |
wenzelm |
header;
|
file |
diff |
annotate
|
| 1999-10-30 |
wenzelm |
Isabelle99;
|
file |
diff |
annotate
|
| 1999-10-22 |
wenzelm |
tuned simplifier trace output; new flag debug_simp
|
file |
diff |
annotate
|
| 1999-10-20 |
wenzelm |
the settings environment is now statically scoped;
|
file |
diff |
annotate
|