| Tue, 07 Nov 1995 13:15:04 +0100 |
clasohm |
added leading "." to HTML filenames
|
file |
diff |
annotate
|
| Fri, 03 Nov 1995 12:00:46 +0100 |
clasohm |
removed image borders from index.html files
|
file |
diff |
annotate
|
| Thu, 02 Nov 1995 14:16:00 +0100 |
clasohm |
removed borders from images in charts;
|
file |
diff |
annotate
|
| Thu, 26 Oct 1995 13:53:04 +0100 |
clasohm |
renamed chart00 and 00-chart to "index"
|
file |
diff |
annotate
|
| Wed, 25 Oct 1995 13:41:45 +0100 |
clasohm |
removed "duplicate" warning from store_thm_db;
|
file |
diff |
annotate
|
| Tue, 24 Oct 1995 13:53:09 +0100 |
clasohm |
added generation of HTML files to thy_read.ML;
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 12:59:52 +0100 |
clasohm |
added removal of theorems if theory is to be reloaded; changed functions for
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:51:49 +0200 |
clasohm |
restored old invocation of use_string till I can make the new version work
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:28:54 +0200 |
clasohm |
added cleanup of global simpset to thy_read;
|
file |
diff |
annotate
|
| Wed, 30 Aug 1995 14:04:39 +0200 |
clasohm |
added check for duplicate theorems in theorem database;
|
file |
diff |
annotate
|
| Tue, 08 Aug 1995 09:27:02 +0200 |
nipkow |
corrected bind_thm: now applies "standard" uniformly.
|
file |
diff |
annotate
|
| Fri, 23 Jun 1995 11:59:06 +0200 |
clasohm |
added a few comments on ThyInfo
|
file |
diff |
annotate
|
| Thu, 22 Jun 1995 12:58:39 +0200 |
clasohm |
changed call of store_thm_db so that it's result is not displayed
|
file |
diff |
annotate
|
| Mon, 29 May 1995 13:55:06 +0200 |
clasohm |
added theorem database which contains axioms and theorems indexed by the
|
file |
diff |
annotate
|
| Wed, 03 May 1995 15:25:30 +0200 |
clasohm |
fixed bug in thy_unchanged that occurred when the .thy file was changed
|
file |
diff |
annotate
|
| Thu, 23 Mar 1995 15:39:13 +0100 |
clasohm |
fixed bug: parent theory wasn't loaded if .thy file was completly read before
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|
| Mon, 23 Jan 1995 12:20:10 +0100 |
clasohm |
simplified get_thm a bit
|
file |
diff |
annotate
|
| Wed, 14 Dec 1994 13:03:09 +0100 |
clasohm |
changed get_thm to search all parent theories if the theorem is not found
|
file |
diff |
annotate
|
| Mon, 12 Dec 1994 10:26:05 +0100 |
wenzelm |
added print_theory that prints stored thms;
|
file |
diff |
annotate
|
| Fri, 09 Dec 1994 13:05:03 +0100 |
clasohm |
added warning for already stored theorem to store_thm
|
file |
diff |
annotate
|
| Wed, 07 Dec 1994 12:34:47 +0100 |
clasohm |
moved first call of store_theory from thy_read.ML to created .thy.ML file
|
file |
diff |
annotate
|
| Tue, 06 Dec 1994 12:50:13 +0100 |
clasohm |
added bind_thm
|
file |
diff |
annotate
|
| Fri, 25 Nov 1994 09:13:49 +0100 |
clasohm |
added qed_goal[w]
|
file |
diff |
annotate
|
| Fri, 18 Nov 1994 13:08:10 +0100 |
clasohm |
added call of store_theory after thy file has been read
|
file |
diff |
annotate
|
| Tue, 06 Sep 1994 14:44:10 +0200 |
clasohm |
renamed base_on into mk_base and moved it to the beginning of the generated
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 15:39:19 +0200 |
wenzelm |
added theory_of_sign, theory_of_thm;
|
file |
diff |
annotate
|
| Fri, 15 Jul 1994 13:30:42 +0200 |
clasohm |
added check for concistency of filename and theory name;
|
file |
diff |
annotate
|
| Fri, 17 Jun 1994 12:43:24 +0200 |
clasohm |
replaced "foldl merge_theories" by "merge_thy_list" in base_on
|
file |
diff |
annotate
|
| Thu, 16 Jun 1994 12:06:56 +0200 |
wenzelm |
base_on: added 'mk_draft' arg;
|
file |
diff |
annotate
|
| Wed, 01 Jun 1994 15:46:11 +0200 |
wenzelm |
restored old functor name;
|
file |
diff |
annotate
|
| Thu, 26 May 1994 13:45:43 +0200 |
clasohm |
changed syntax of use_string
|
file |
diff |
annotate
|
| Thu, 19 May 1994 16:30:56 +0200 |
wenzelm |
(was Thy/read.ML)
|
file |
diff |
annotate
|