2000-12-13 |
wenzelm |
* print modes "brackets" and "no_brackets" control output of nested =>
|
file |
diff |
annotate
|
2000-12-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2000-12-06 |
bauerg |
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
|
file |
diff |
annotate
|
2000-11-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2000-11-30 |
wenzelm |
misc;
|
file |
diff |
annotate
|
2000-11-23 |
wenzelm |
* HOL: syntax or "abs";
|
file |
diff |
annotate
|
2000-11-16 |
paulson |
CTT
|
file |
diff |
annotate
|
2000-11-13 |
nipkow |
Removed > and >=
|
file |
diff |
annotate
|
2000-11-10 |
wenzelm |
* added overloaded operations "inverse" and "divide" (infix "/");
|
file |
diff |
annotate
|
2000-11-10 |
nipkow |
> etc
|
file |
diff |
annotate
|
2000-11-08 |
nipkow |
subgoals
|
file |
diff |
annotate
|
2000-11-06 |
wenzelm |
* Isar/HOL: method 'induct' now handles non-atomic goals; as a
|
file |
diff |
annotate
|
2000-11-04 |
wenzelm |
misc stuff;
|
file |
diff |
annotate
|
2000-10-25 |
wenzelm |
added HOL/Library/List_Prefix;
|
file |
diff |
annotate
|
2000-10-24 |
wenzelm |
* support sub/super scripts (for single symbols only), input syntax is
|
file |
diff |
annotate
|
2000-10-23 |
wenzelm |
* HOL: default proof step now includes 'intro_classes';
|
file |
diff |
annotate
|
2000-10-23 |
paulson |
contrapos
|
file |
diff |
annotate
|
2000-10-18 |
wenzelm |
* HOL/Library: a collection of generic theories to be used together
|
file |
diff |
annotate
|
2000-10-16 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-10-06 |
wenzelm |
* HOL/IMPP: extension of IMP with local variables and mutually
|
file |
diff |
annotate
|
2000-10-05 |
wenzelm |
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
|
file |
diff |
annotate
|
2000-10-03 |
wenzelm |
removed "symbols" syntax for constant "override";
|
file |
diff |
annotate
|
2000-10-02 |
wenzelm |
improved t.weak_case_cong text;
|
file |
diff |
annotate
|
2000-09-28 |
wenzelm |
Isabelle99-1 (October 2000);
|
file |
diff |
annotate
|
2000-09-26 |
wenzelm |
HOL/MicroJava;
|
file |
diff |
annotate
|
2000-09-23 |
paulson |
renaming the inverse image operator in HOL
|
file |
diff |
annotate
|
2000-09-15 |
wenzelm |
cleaned up and prepared for Isabelle99-1;
|
file |
diff |
annotate
|
2000-09-15 |
wenzelm |
system: isatool installfonts may handle X-Symbol fonts as well;
|
file |
diff |
annotate
|
2000-09-15 |
paulson |
renamed the select rules
|
file |
diff |
annotate
|
2000-09-12 |
wenzelm |
renamed atts: rulify to rule_format, elimify to elim_format;
|
file |
diff |
annotate
|
2000-09-12 |
wenzelm |
replaced "delrule" by "rule del";
|
file |
diff |
annotate
|
2000-09-07 |
wenzelm |
HOL: qed_spec_mp now also removes bounded ALL;
|
file |
diff |
annotate
|
2000-09-06 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-09-05 |
paulson |
meson_tac
|
file |
diff |
annotate
|
2000-09-02 |
wenzelm |
* HOL/Lambda: converted into new-style theory and document;
|
file |
diff |
annotate
|
2000-08-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2000-08-30 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-08-30 |
wenzelm |
fixed name;
|
file |
diff |
annotate
|
2000-08-30 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-08-29 |
wenzelm |
* 'pr' command: optional argument for ProofContext.prems_limit;
|
file |
diff |
annotate
|
2000-08-28 |
wenzelm |
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
|
file |
diff |
annotate
|
2000-08-28 |
wenzelm |
* \isabellestyle{it} produces near math mode output;
|
file |
diff |
annotate
|
2000-08-18 |
paulson |
new example ZF/ex/NatSum
|
file |
diff |
annotate
|
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
|