| Thu, 03 Nov 2005 02:37:09 +0100 |
huffman |
reimplement copy_def to use data constructor constants
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 02:19:48 +0100 |
huffman |
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
|
file |
diff |
annotate
|
| Wed, 02 Nov 2005 14:46:51 +0100 |
wenzelm |
dist_eqI: the_context();
|
file |
diff |
annotate
|
| Tue, 25 Oct 2005 18:18:49 +0200 |
wenzelm |
avoid legacy goals;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:38 +0200 |
wenzelm |
OldGoals;
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 03:02:18 +0200 |
huffman |
domain package generates compactness lemmas for new constructors
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 03:55:39 +0200 |
huffman |
replaced foldr' with foldr1
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:25 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 18:28:36 +0200 |
huffman |
use qualified names for all constants
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:13:59 +0200 |
wenzelm |
get_thm(s): Name;
|
file |
diff |
annotate
|
| Sat, 18 Jun 2005 00:33:27 +0200 |
huffman |
make match_rews into simp rules by default
|
file |
diff |
annotate
|
| Wed, 15 Jun 2005 23:35:43 +0200 |
huffman |
Domain package uses ContProc for beta reduction
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 23:44:37 +0200 |
huffman |
in domain declarations, selector names are now optional
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 03:35:15 +0200 |
huffman |
up_eq and up_less in default simpset now
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 02:27:19 +0200 |
huffman |
faster proofs of inverts and injects lemmas, with fewer strictness hypotheses
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 00:24:33 +0200 |
huffman |
Domain package generates match functions for new datatypes, for use with the fixrec package
|
file |
diff |
annotate
|
| Sat, 16 Apr 2005 00:17:52 +0200 |
huffman |
speed improvements for the domain package
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 17:59:48 +0100 |
berghofe |
Adapted to modified interface of PureThy.get_thm(s).
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 29 May 2004 14:59:24 +0200 |
wenzelm |
Sign.infer_types: Sign.pp;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2002 14:32:56 +0200 |
berghofe |
Replaced nat_ind_tac by induct_tac.
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 18:42:00 +0100 |
wenzelm |
adapted to new-style theories;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:41:26 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:26:55 +0200 |
berghofe |
Renamed functions % and %% to avoid clash with syntax for proof terms.
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:36:30 +0100 |
nipkow |
` -> $
|
file |
diff |
annotate
|
| Tue, 17 Oct 2000 10:20:43 +0200 |
paulson |
tidying and renaming of contrapos rules
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 13:28:31 +0100 |
wenzelm |
adapted to new PureThy.add_thms etc.;
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 11:23:41 +0100 |
oheimb |
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
|
file |
diff |
annotate
|
| Thu, 21 Oct 1999 18:46:33 +0200 |
wenzelm |
get_thm;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 13:54:51 +0100 |
wenzelm |
eliminated tthm type and Attribute structure;
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 12:17:20 +0200 |
slotosch |
eliminated fabs,fapp.
|
file |
diff |
annotate
|
| 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
|