| Sat, 13 Mar 2010 16:44:12 +0100 |
wenzelm |
removed old CVS Ids;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 21:20:56 +0200 |
wenzelm |
simultaneous use_thys;
|
file |
diff |
annotate
|
| Tue, 08 Jun 2004 16:22:30 +0200 |
paulson |
Groups, Rings and supporting lemmas
|
file |
diff |
annotate
|
| Fri, 16 Nov 2001 22:11:19 +0100 |
wenzelm |
Ntree and Brouwer converted and moved to ZF/Induct;
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 18:08:19 +0100 |
wenzelm |
TF and Term moved to ZF/Induct;
|
file |
diff |
annotate
|
| Wed, 14 Nov 2001 23:21:05 +0100 |
wenzelm |
removed BT, Data, Enum (see ZF/Induct);
|
file |
diff |
annotate
|
| Wed, 07 Nov 2001 12:29:07 +0100 |
paulson |
reorganization of the ZF examples
|
file |
diff |
annotate
|
| Fri, 06 Jul 2001 16:04:32 +0200 |
paulson |
two Isar tactic scripts
|
file |
diff |
annotate
|
| Sat, 03 Feb 2001 12:41:38 +0100 |
paulson |
commutation theory, ported by Sidi Ehmety
|
file |
diff |
annotate
|
| Fri, 18 Aug 2000 12:31:20 +0200 |
paulson |
new example ZF/ex/NatSum
|
file |
diff |
annotate
|
| Tue, 30 May 2000 16:08:38 +0200 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
| Thu, 11 Mar 1999 13:20:35 +0100 |
wenzelm |
removed foo_build_completed -- now handled by session management (via usedir);
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:53:24 +0100 |
paulson |
fixed comment
|
file |
diff |
annotate
|
| Tue, 22 Sep 1998 15:24:39 +0200 |
paulson |
re-organized for the new directory Integ
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:18:03 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 13:01:07 +0100 |
paulson |
Better indentation
|
file |
diff |
annotate
|
| Thu, 13 Jun 1996 16:22:37 +0200 |
paulson |
New example of GCDs and divides relation
|
file |
diff |
annotate
|
| Tue, 26 Mar 1996 12:01:13 +0100 |
paulson |
Now loads Mutil example
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Tue, 21 Nov 1995 12:43:09 +0100 |
clasohm |
removed make_chart;
|
file |
diff |
annotate
|
| Tue, 24 Oct 1995 14:50:24 +0100 |
clasohm |
added calls of init_html and make_chart
|
file |
diff |
annotate
|
| Mon, 16 Oct 1995 16:32:56 +0100 |
paulson |
Added the new Limit.{thy,ML} example
|
file |
diff |
annotate
|
| Thu, 16 Mar 1995 00:00:30 +0100 |
lcp |
Removed exception handlers, as they are now in ZF/Makefile.
|
file |
diff |
annotate
|
| Tue, 28 Feb 1995 10:53:56 +0100 |
lcp |
No longer calls maketest; instead, the Makefile writes the file
|
file |
diff |
annotate
|
| Wed, 07 Sep 1994 17:28:53 +0200 |
lcp |
addition of ZF/ex/twos_compl.thy
|
file |
diff |
annotate
|
| Wed, 17 Aug 1994 10:38:37 +0200 |
lcp |
ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
|
file |
diff |
annotate
|
| Mon, 15 Aug 1994 18:27:50 +0200 |
lcp |
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 12:28:46 +0200 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| Wed, 27 Jul 1994 16:03:16 +0200 |
lcp |
Addition of infinite branching datatypes
|
file |
diff |
annotate
|
| Fri, 06 May 1994 15:35:35 +0200 |
lcp |
renaming/removal of filenames to correct case
|
file |
diff |
annotate
|
| Wed, 01 Dec 1993 17:40:27 +0100 |
lcp |
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
|
file |
diff |
annotate
|
| Tue, 16 Nov 1993 14:26:15 +0100 |
clasohm |
changed use_thy's parameter to exact theory name
|
file |
diff |
annotate
|
| Mon, 15 Nov 1993 14:41:25 +0100 |
lcp |
changed all co- and co_ to co
|
file |
diff |
annotate
|
| Mon, 08 Nov 1993 17:52:24 +0100 |
lcp |
Minor changes; addition of counit.ML
|
file |
diff |
annotate
|
| Thu, 04 Nov 1993 14:12:31 +0100 |
clasohm |
renamed twos-compl.ML to twos_compl.ML
|
file |
diff |
annotate
|
| Fri, 22 Oct 1993 13:44:27 +0100 |
clasohm |
renamed some files
|
file |
diff |
annotate
|
| Fri, 15 Oct 1993 10:25:23 +0100 |
lcp |
ZF/ex/tf/tree,forest_unfold: streamlined the proofs
|
file |
diff |
annotate
|
| Wed, 06 Oct 1993 14:45:04 +0100 |
clasohm |
changed filenames to lower case name of theory the file contains
|
file |
diff |
annotate
|
| Thu, 30 Sep 1993 10:54:01 +0100 |
lcp |
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|