| Tue, 19 Jan 1999 12:59:55 +0100 |
paulson |
tidied freeness reasoning
|
changeset |
files
|
| Tue, 19 Jan 1999 12:56:27 +0100 |
paulson |
freeness reasoning: T.free_iffs
|
changeset |
files
|
| Tue, 19 Jan 1999 11:46:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 19 Jan 1999 11:18:11 +0100 |
paulson |
removal of the (thm list) argument of mk_cases
|
changeset |
files
|
| Tue, 19 Jan 1999 11:16:39 +0100 |
paulson |
tidied; added dest_eq
|
changeset |
files
|
| Tue, 19 Jan 1999 11:16:07 +0100 |
paulson |
simplified thanks to the arithmetic prover
|
changeset |
files
|
| Tue, 19 Jan 1999 11:15:40 +0100 |
paulson |
updated comments
|
changeset |
files
|
| Tue, 19 Jan 1999 11:15:03 +0100 |
paulson |
a simplification by G Bella
|
changeset |
files
|
| Mon, 18 Jan 1999 21:12:42 +0100 |
wenzelm |
structure Graph = Graph;
|
changeset |
files
|
| Mon, 18 Jan 1999 21:09:34 +0100 |
wenzelm |
GraphFun (generic directed graphs);
|
changeset |
files
|
| Mon, 18 Jan 1999 21:08:27 +0100 |
wenzelm |
added General/graph.ML: generic direct graphs;
|
changeset |
files
|
| Fri, 15 Jan 1999 16:13:31 +0100 |
oheimb |
removed empty line (in case of empty begin_state marker) before Level line
|
changeset |
files
|
| Thu, 14 Jan 1999 14:39:11 +0100 |
nipkow |
Removed superfluous arith rules from metric_simps
|
changeset |
files
|
| Thu, 14 Jan 1999 14:29:52 +0100 |
nipkow |
More Arith.
|
changeset |
files
|
| Thu, 14 Jan 1999 13:20:02 +0100 |
nipkow |
Fixed old bug: selection of constant to be split should depend not just on
|
changeset |
files
|
| Thu, 14 Jan 1999 13:19:12 +0100 |
nipkow |
nat_arith_tac -> arith_tac
|
changeset |
files
|
| Thu, 14 Jan 1999 13:18:09 +0100 |
nipkow |
More arith refinements.
|
changeset |
files
|
| Thu, 14 Jan 1999 12:32:13 +0100 |
wenzelm |
tuned README;
|
changeset |
files
|
| Thu, 14 Jan 1999 12:32:00 +0100 |
wenzelm |
Pure/General/symbol.ML;
|
changeset |
files
|
| Thu, 14 Jan 1999 12:23:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 13 Jan 1999 16:38:52 +0100 |
paulson |
deleted the appendices because documentation exists in the HOL and ZF manuals
|
changeset |
files
|
| Wed, 13 Jan 1999 16:38:16 +0100 |
paulson |
defined dquotesoff
|
changeset |
files
|
| Wed, 13 Jan 1999 16:38:02 +0100 |
paulson |
new manual ZF
|
changeset |
files
|
| Wed, 13 Jan 1999 16:36:36 +0100 |
paulson |
the separate FOL and ZF logics manual, with new material on datatypes and
|
changeset |
files
|
| Wed, 13 Jan 1999 16:30:53 +0100 |
paulson |
removal of FOL and ZF
|
changeset |
files
|
| Wed, 13 Jan 1999 16:29:50 +0100 |
paulson |
minor updates on inductive definitions and datatypes
|
changeset |
files
|
| Wed, 13 Jan 1999 15:18:02 +0100 |
wenzelm |
fixed titles;
|
changeset |
files
|
| Wed, 13 Jan 1999 15:14:47 +0100 |
paulson |
tidying of datatype and inductive definitions
|
changeset |
files
|
| Wed, 13 Jan 1999 12:44:33 +0100 |
wenzelm |
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
|
changeset |
files
|
| Wed, 13 Jan 1999 12:16:34 +0100 |
nipkow |
Refined arithmetic.
|
changeset |
files
|