| Wed, 29 Apr 1998 11:36:08 +0200 |
wenzelm |
adapted to new PureThy.add_tthmss;
|
file |
diff |
annotate
|
| Tue, 24 Mar 1998 15:57:18 +0100 |
oheimb |
added cproj', and therefore extended prj
|
file |
diff |
annotate
|
| Tue, 10 Mar 1998 18:33:13 +0100 |
oheimb |
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:29:56 +0100 |
wenzelm |
changed Pure/Sequence interface -- isatool fixseq;
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 12:59:20 +0100 |
wenzelm |
tuned infer_types interface;
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 16:27:13 +0100 |
wenzelm |
structure BasisLibrary;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 14:06:27 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 13:01:07 +0100 |
paulson |
New way of referring to Basis Library
|
file |
diff |
annotate
|
| Thu, 30 Oct 1997 14:19:01 +0100 |
oheimb |
domain package:
|
file |
diff |
annotate
|
| Wed, 29 Oct 1997 14:23:49 +0100 |
oheimb |
debugging concerning sort variables
|
file |
diff |
annotate
|
| Mon, 27 Oct 1997 11:34:33 +0100 |
oheimb |
adapted domain and ax_ops package for name spaces
|
file |
diff |
annotate
|
| Sun, 25 May 1997 11:07:52 +0200 |
slotosch |
eliminated the constant less by the introduction of the axclass sq_ord
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 18:51:14 +0200 |
nipkow |
Updates because nat_ind_tac no longer appends "1" to the ind.var.
|
file |
diff |
annotate
|
| Wed, 18 Dec 1996 15:19:42 +0100 |
oheimb |
The previous log message was wrong. The correct one is:
|
file |
diff |
annotate
|
| Wed, 18 Dec 1996 15:16:13 +0100 |
oheimb |
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
|
file |
diff |
annotate
|
| Fri, 29 Nov 1996 12:16:57 +0100 |
oheimb |
modified file headers
|
file |
diff |
annotate
|
| Thu, 28 Nov 1996 10:50:43 +0100 |
paulson |
Replaced map...~~ by ListPair.map
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 15:14:23 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
file |
diff |
annotate
|
| Thu, 27 Jun 1996 15:24:17 +0200 |
oheimb |
re-added when_funs to library.ML
|
file |
diff |
annotate
|
| Wed, 26 Jun 1996 17:38:34 +0200 |
oheimb |
function names in when_rews now meta-quantified
|
file |
diff |
annotate
|
| Fri, 31 May 1996 20:25:59 +0200 |
oheimb |
adapted use of monofun_cfun_arg
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 17:01:51 +0200 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 13:28:50 +0200 |
oheimb |
Removed 8bit characters used by mistake
|
file |
diff |
annotate
|
| Wed, 03 Apr 1996 20:08:27 +0200 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 03 Apr 1996 19:27:14 +0200 |
oheimb |
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 06 Oct 1995 17:25:24 +0100 |
regensbu |
added 8bit pragmas
|
file |
diff |
annotate
|