| 2001-08-09 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|
| 2001-08-08 |
wenzelm |
* HOL: syntax translations now work properly with numerals and records
|
file |
diff |
annotate
|
| 2001-08-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-08-07 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-07-20 |
wenzelm |
HOL: added "The";
|
file |
diff |
annotate
|
| 2001-07-03 |
paulson |
GroupTheory
|
file |
diff |
annotate
|
| 2001-06-05 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-05-21 |
paulson |
ZF: division
|
file |
diff |
annotate
|
| 2001-05-18 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-04-09 |
paulson |
Isar hint
|
file |
diff |
annotate
|
| 2001-02-23 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|
| 2001-02-21 |
oheimb |
added split_conv_tac (also to claset()) as an optimization
|
file |
diff |
annotate
|
| 2001-02-20 |
oheimb |
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
|
file |
diff |
annotate
|
| 2001-02-15 |
oheimb |
added missiong word
|
file |
diff |
annotate
|
| 2001-02-14 |
wenzelm |
isatool install handles KDE version 1 or 2;
|
file |
diff |
annotate
|
| 2001-02-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-02-11 |
wenzelm |
more robust selection of calculational rules;
|
file |
diff |
annotate
|
| 2001-02-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-02-10 |
ballarin |
Updates to HOL/Algebra:
|
file |
diff |
annotate
|
| 2001-02-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-02-04 |
wenzelm |
* no_document ML operator temporarily disables LaTeX document
|
file |
diff |
annotate
|
| 2001-02-03 |
wenzelm |
HOL: inductive package no longer splits induction rule aggressively,
|
file |
diff |
annotate
|
| 2001-02-01 |
wenzelm |
* Pure: 'thms_containing' now takes actual terms as arguments;
|
file |
diff |
annotate
|
| 2001-01-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-01-24 |
wenzelm |
* Document preparation: renamed standard symbols \<ll> to \<lless> and
|
file |
diff |
annotate
|
| 2001-01-23 |
wenzelm |
added HOL-Unix example;
|
file |
diff |
annotate
|
| 2001-01-19 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-15 |
wenzelm |
* HOL/datatype: induction rule for arbitrarily branching datatypes is
|
file |
diff |
annotate
|
| 2001-01-11 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-10 |
wenzelm |
isatool unsymbolize;
|
file |
diff |
annotate
|
| 2001-01-10 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2001-01-10 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-06 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-05 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2001-01-03 |
wenzelm |
* Isar/HOL: added 'recdef_tc' command;
|
file |
diff |
annotate
|
| 2001-01-01 |
paulson |
Hyperreal
|
file |
diff |
annotate
|
| 2000-12-22 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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
|