| Mon, 23 Jun 1997 10:42:03 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:30:52 +0200 |
paulson |
Moved "less_eq" to NatDef from Arith
|
file |
diff |
annotate
|
| Tue, 27 May 1997 13:23:53 +0200 |
paulson |
New theorem le_Suc_eq
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:39:57 +0200 |
paulson |
Renamed lessD to Suc_leI
|
file |
diff |
annotate
|
| Fri, 23 May 1997 09:17:26 +0200 |
nipkow |
Added overloaded function `size' for all datatypes.
|
file |
diff |
annotate
|
| Thu, 22 May 1997 13:05:52 +0200 |
nipkow |
Added rotation to exhaust_tac.
|
file |
diff |
annotate
|
| Thu, 22 May 1997 09:20:28 +0200 |
nipkow |
Added exhaustion thm and exhaust_tac for each datatype.
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:39:32 +0200 |
paulson |
New pattern-matching definition of pred_nat
|
file |
diff |
annotate
|
| Thu, 08 May 1997 11:44:59 +0200 |
nipkow |
Modified def of Least, which, as Markus correctly complained, looked like
|
file |
diff |
annotate
|
| Wed, 30 Apr 1997 13:39:56 +0200 |
paulson |
Fixed clasets so that blast_tac would work
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 18:06:46 +0200 |
nipkow |
Introduced a generic "induct_tac" which picks up the right induction scheme
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:18:29 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Fri, 11 Apr 1997 15:21:36 +0200 |
paulson |
Yet more fast_tac->blast_tac, and other tidying
|
file |
diff |
annotate
|
| Wed, 09 Apr 1997 12:32:04 +0200 |
paulson |
Using Blast_tac
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 11:18:52 +0200 |
paulson |
Calls Blast_tac
|
file |
diff |
annotate
|
| Tue, 04 Mar 1997 10:48:36 +0100 |
paulson |
Renamed constant "not" to "Not"
|
file |
diff |
annotate
|
| Tue, 25 Feb 1997 15:05:14 +0100 |
pusch |
function nat_add_primrec added to allow primrec definitions over nat
|
file |
diff |
annotate
|
| Wed, 12 Feb 1997 18:53:59 +0100 |
nipkow |
New class "order" and accompanying changes.
|
file |
diff |
annotate
|