| 1999-10-13 |
berghofe |
Eliminated mutual_induct_tac.
|
file |
diff |
annotate
|
| 1999-10-08 |
wenzelm |
theorem database now also indexes constants "Trueprop", "all",
|
file |
diff |
annotate
|
| 1999-10-08 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-10-07 |
berghofe |
Documented changes to HOL/inductive and function thm_deps.
|
file |
diff |
annotate
|
| 1999-10-04 |
wenzelm |
added BVC;
|
file |
diff |
annotate
|
| 1999-09-29 |
wenzelm |
proper handling of dangling sort hypotheses (at last!);
|
file |
diff |
annotate
|
| 1999-09-28 |
nipkow |
incompatibility solver
|
file |
diff |
annotate
|
| 1999-09-24 |
wenzelm |
* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
|
file |
diff |
annotate
|
| 1999-09-24 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-09-06 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| 1999-09-03 |
wenzelm |
added bind_thms;
|
file |
diff |
annotate
|
| 1999-09-03 |
paulson |
new SVC url
|
file |
diff |
annotate
|
| 1999-09-01 |
wenzelm |
structures Vartab / Termtab (instances of TableFun);
|
file |
diff |
annotate
|
| 1999-08-23 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-23 |
wenzelm |
record_simproc;
|
file |
diff |
annotate
|
| 1999-08-23 |
nipkow |
simplifier flex heads.
|
file |
diff |
annotate
|
| 1999-08-23 |
berghofe |
Moved sum_case to theory HOL/Datatype.
|
file |
diff |
annotate
|
| 1999-08-21 |
wenzelm |
real numerals;
|
file |
diff |
annotate
|
| 1999-08-19 |
wenzelm |
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
|
file |
diff |
annotate
|
| 1999-08-19 |
paulson |
defer_recdef
|
file |
diff |
annotate
|
| 1999-08-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-18 |
wenzelm |
sum_case renamed to basic_sum_case;
|
file |
diff |
annotate
|
| 1999-08-18 |
wenzelm |
replaced 'ProofGeneral' by 'Proof General';
|
file |
diff |
annotate
|
| 1999-08-17 |
wenzelm |
replaced HOL_quantifiers flag by "HOL" print mode;
|
file |
diff |
annotate
|
| 1999-08-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-16 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-08-11 |
nipkow |
Removed
|
file |
diff |
annotate
|
| 1999-08-09 |
wenzelm |
theory loader actions;
|
file |
diff |
annotate
|
| 1999-08-03 |
paulson |
SVC
|
file |
diff |
annotate
|
| 1999-07-28 |
wenzelm |
HOL-Real target now builds an actual image;
|
file |
diff |
annotate
|
| 1999-07-28 |
paulson |
LK
|
file |
diff |
annotate
|
| 1999-07-19 |
berghofe |
Datatype package now handles arbitrarily branching datatypes.
|
file |
diff |
annotate
|
| 1999-07-08 |
wenzelm |
theorems involving oracles are now printed with a suffixed [!];
|
file |
diff |
annotate
|
| 1999-07-08 |
paulson |
integer division
|
file |
diff |
annotate
|
| 1999-06-07 |
wenzelm |
reset HOL_quantifiers by default;
|
file |
diff |
annotate
|
| 1999-05-31 |
wenzelm |
Isabelle manuals now also available as PDF;
|
file |
diff |
annotate
|
| 1999-05-18 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-05-03 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-04-27 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-04-22 |
wenzelm |
recdef (TFL) now requires theory Recdef;
|
file |
diff |
annotate
|
| 1999-04-21 |
wenzelm |
Isamode 2.6 requires patch;
|
file |
diff |
annotate
|
| 1999-04-16 |
wenzelm |
loadpath replaced;
|
file |
diff |
annotate
|
| 1999-04-14 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-04-13 |
wenzelm |
improved isatool install;
|
file |
diff |
annotate
|
| 1999-04-12 |
wenzelm |
ML_PLATFORM;
|
file |
diff |
annotate
|
| 1999-03-18 |
nipkow |
* New bounded quantifier syntax (input only):
|
file |
diff |
annotate
|
| 1999-03-17 |
wenzelm |
HOL/typedef: fixed type inference for representing set;
|
file |
diff |
annotate
|
| 1999-03-10 |
wenzelm |
updated;
|
file |
diff |
annotate
|
| 1999-02-11 |
wenzelm |
Symbol.output subject to print mode;
|
file |
diff |
annotate
|
| 1999-02-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-02-08 |
wenzelm |
path element specification '~~' refers to '$ISABELLE_HOME';
|
file |
diff |
annotate
|
| 1999-02-03 |
paulson |
inj
|
file |
diff |
annotate
|
| 1999-01-27 |
nipkow |
arith_tac for min/max
|
file |
diff |
annotate
|
| 1999-01-27 |
paulson |
ZF typechecking
|
file |
diff |
annotate
|
| 1999-01-19 |
paulson |
removal of the (thm list) argument of mk_cases
|
file |
diff |
annotate
|
| 1999-01-14 |
nipkow |
More Arith.
|
file |
diff |
annotate
|
| 1999-01-07 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
| 1999-01-07 |
paulson |
if-then-else syntax for ZF
|
file |
diff |
annotate
|
| 1999-01-06 |
paulson |
primrec, induct_tac
|
file |
diff |
annotate
|
| 1999-01-05 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|