Thu, 24 Apr 1997 17:59:55 +0200 |
nipkow |
rename_params_rule used to check if the new name clashed with a free name in
|
changeset |
files
|
Thu, 24 Apr 1997 17:51:27 +0200 |
mueller |
deleted definitions for blift and plift
|
changeset |
files
|
Thu, 24 Apr 1997 17:50:34 +0200 |
mueller |
Complete Redesign of Theory, main points are:
|
changeset |
files
|
Thu, 24 Apr 1997 17:40:30 +0200 |
mueller |
added liftpair definition
|
changeset |
files
|
Thu, 24 Apr 1997 17:38:33 +0200 |
mueller |
only in comments
|
changeset |
files
|
Thu, 24 Apr 1997 17:35:47 +0200 |
mueller |
minor changes due to more powerful continuity check in Lift3.ML
|
changeset |
files
|
Thu, 24 Apr 1997 17:04:07 +0200 |
mueller |
added some comments;
|
changeset |
files
|
Thu, 24 Apr 1997 11:21:46 +0200 |
paulson |
Addition of printed tracing. Also some tidying
|
changeset |
files
|
Thu, 24 Apr 1997 11:20:56 +0200 |
paulson |
A bit of tidying
|
changeset |
files
|
Thu, 24 Apr 1997 10:40:01 +0200 |
oheimb |
added dependencies on ax_ops/*.ML and domain/*.ML
|
changeset |
files
|
Thu, 24 Apr 1997 10:39:00 +0200 |
oheimb |
changed priority of '%': now no parenteses needed for '[...] == %x. [...]'
|
changeset |
files
|
Thu, 24 Apr 1997 09:34:59 +0200 |
slotosch |
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML
|
changeset |
files
|
Wed, 23 Apr 1997 13:23:05 +0200 |
nipkow |
Added NatDef
|
changeset |
files
|
Wed, 23 Apr 1997 11:20:18 +0200 |
paulson |
Necessary inclusion of depth bound into blast_tac call
|
changeset |
files
|