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
|
1999-01-04 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
1998-12-11 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
1998-12-04 |
paulson |
locales
|
file |
diff |
annotate
|
1998-11-25 |
wenzelm |
removed prs / prs_fn;
|
file |
diff |
annotate
|
1998-11-18 |
paulson |
Finally removing "Compl" from HOL
|
file |
diff |
annotate
|
1998-10-30 |
wenzelm |
tuned current_goals_markers;
|
file |
diff |
annotate
|
1998-10-22 |
wenzelm |
current_goals_markers;
|
file |
diff |
annotate
|
1998-10-22 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
1998-10-22 |
paulson |
locales
|
file |
diff |
annotate
|