| 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
|
| 1998-06-23 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 1998-06-20 |
wenzelm |
renamed Thm(s) back to thm(s);
|
file |
diff |
annotate
|
| 1998-06-18 |
wenzelm |
new toplevel commands `Goal' and `Goalw';
|
file |
diff |
annotate
|
| 1998-06-18 |
wenzelm |
renamed thm(s) to Thm(s);
|
file |
diff |
annotate
|
| 1998-06-17 |
nipkow |
Goal and Goalw
|
file |
diff |
annotate
|
| 1998-06-10 |
wenzelm |
new type-safe user interface for theory data;
|
file |
diff |
annotate
|
| 1998-06-05 |
wenzelm |
* improved the theory data mechanism to support real encapsulation;
|
file |
diff |
annotate
|
| 1998-05-28 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
| 1998-05-14 |
oheimb |
extended addsplits and delsplits to handle also split rules for assumptions
|
file |
diff |
annotate
|
| 1998-05-13 |
wenzelm |
HOL/record: now includes concrete syntax for record terms;
|
file |
diff |
annotate
|
| 1998-05-06 |
paulson |
HOL/Update
|
file |
diff |
annotate
|
| 1998-05-01 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 1998-05-01 |
paulson |
"let" is no longer restricted to FOL terms and allows any logical terms
|
file |
diff |
annotate
|
| 1998-04-29 |
wenzelm |
new theory section 'setup';
|
file |
diff |
annotate
|
| 1998-04-29 |
wenzelm |
new theory section 'nonterminals';
|
file |
diff |
annotate
|
| 1998-04-29 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| 1998-04-27 |
oheimb |
cleanup for split_all_tac as wrapper in claset()
|
file |
diff |
annotate
|
| 1998-04-27 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 1998-04-24 |
oheimb |
improved split_all_tac significantly
|
file |
diff |
annotate
|
| 1998-04-24 |
paulson |
tidied; div & mod
|
file |
diff |
annotate
|
| 1998-04-24 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| 1998-04-10 |
paulson |
bug fixes
|
file |
diff |
annotate
|
| 1998-04-07 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| 1998-04-03 |
paulson |
UNITY
|
file |
diff |
annotate
|
| 1998-04-02 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| 1998-03-16 |
paulson |
inverse -> converse
|
file |
diff |
annotate
|