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
|
1998-10-21 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
1998-10-21 |
nipkow |
Tutorial
|
file |
diff |
annotate
|
1998-10-21 |
wenzelm |
tuned (all proofs are INSTABLE by David's definition of instability);
|
file |
diff |
annotate
|
1998-10-19 |
oheimb |
layout
|
file |
diff |
annotate
|
1998-10-16 |
nipkow |
2. The simplifier now knows a little bit about nat-arithmetic.
|
file |
diff |
annotate
|
1998-10-16 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
1998-10-15 |
paulson |
integer simprocs
|
file |
diff |
annotate
|
1998-09-25 |
wenzelm |
isatool logo;
|
file |
diff |
annotate
|
1998-09-23 |
paulson |
unary minus
|
file |
diff |
annotate
|
1998-09-21 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
1998-09-21 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
1998-09-15 |
paulson |
From Compl(A) to -A
|
file |
diff |
annotate
|
1998-09-10 |
paulson |
equals0D
|
file |
diff |
annotate
|
1998-09-04 |
nipkow |
Function 'upt'
|
file |
diff |
annotate
|
1998-08-28 |
wenzelm |
* print mode 'emacs' reserved for Isamode;
|
file |
diff |
annotate
|
1998-08-27 |
wenzelm |
* Pure: ML function 'theory_of' replaced by 'theory';
|
file |
diff |
annotate
|
1998-08-24 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
1998-08-24 |
wenzelm |
isatool install;
|
file |
diff |
annotate
|
1998-08-18 |
paulson |
ZF.thy
|
file |
diff |
annotate
|
1998-08-13 |
paulson |
stac
|
file |
diff |
annotate
|
1998-08-08 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
1998-08-06 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
1998-08-06 |
paulson |
disjointness
|
file |
diff |
annotate
|
1998-08-04 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
1998-07-31 |
berghofe |
Replaced nat.exhaustion by nat.exhaust
|
file |
diff |
annotate
|
1998-07-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
1998-07-30 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
1998-07-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
1998-07-17 |
paulson |
ZF: Main, Update
|
file |
diff |
annotate
|
1998-07-15 |
nipkow |
disjoint
|
file |
diff |
annotate
|
1998-07-14 |
paulson |
new stac
|
file |
diff |
annotate
|
1998-07-14 |
nipkow |
inj_on
|
file |
diff |
annotate
|
1998-07-10 |
wenzelm |
the distribution now includes Isabelle icons: see
|
file |
diff |
annotate
|
1998-07-03 |
wenzelm |
several new basic modules made available for general use;
|
file |
diff |
annotate
|
1998-07-03 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
1998-07-03 |
wenzelm |
reorganized the main HOL image;
|
file |
diff |
annotate
|
1998-07-01 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
1998-07-01 |
paulson |
HOL-Real
|
file |
diff |
annotate
|
1998-06-25 |
wenzelm |
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
|
file |
diff |
annotate
|
1998-06-24 |
nipkow |
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
|
file |
diff |
annotate
|
1998-06-24 |
paulson |
removed duplicate entry for Goal
|
file |
diff |
annotate
|