| Mon, 29 Jun 1998 10:32:06 +0200 |
wenzelm |
use_text: verbose flag;
|
file |
diff |
annotate
|
| Mon, 15 Jun 1998 11:06:00 +0200 |
wenzelm |
use_text replaces use_strings;
|
file |
diff |
annotate
|
| Mon, 25 May 1998 21:28:07 +0200 |
wenzelm |
tuned store_theory;
|
file |
diff |
annotate
|
| Wed, 17 Dec 1997 15:43:22 +0100 |
wenzelm |
tuned tmp file name;
|
file |
diff |
annotate
|
| Fri, 05 Dec 1997 08:01:03 +0100 |
wenzelm |
tmp_name;
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 16:25:35 +0100 |
wenzelm |
adapted to new Use, File structs;
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 12:03:48 +0100 |
wenzelm |
removed old thy data stuff;
|
file |
diff |
annotate
|
| Tue, 28 Oct 1997 17:34:12 +0100 |
wenzelm |
always reload .ML *and* .thy file;
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:18:49 +0200 |
wenzelm |
merge: default to ProtoPure.thy;
|
file |
diff |
annotate
|
| Thu, 23 Oct 1997 12:43:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Oct 1997 17:48:06 +0200 |
wenzelm |
commit;
|
file |
diff |
annotate
|
| Wed, 15 Oct 1997 15:15:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 17:41:20 +0200 |
wenzelm |
fully qualified name: Theory.merge_thy_list;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 14:42:44 +0200 |
wenzelm |
renamed use_string to use_strings;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 14:11:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 11:52:16 +0200 |
wenzelm |
eliminated ThySynData and ThySynFun;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 00:23:01 +0200 |
berghofe |
Moved several functions:
|
file |
diff |
annotate
|
| Fri, 25 Jul 1997 13:17:14 +0200 |
wenzelm |
remove references to simplifier.ML;
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 13:35:36 +0200 |
wenzelm |
tuned warning;
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 18:03:23 +0200 |
nipkow |
get_thydata accesses the second component of the data field. This component
|
file |
diff |
annotate
|
| Mon, 16 Dec 1996 10:03:30 +0100 |
wenzelm |
now uses SymbolInput.use;
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 10:54:16 +0100 |
paulson |
Converted I/O operatios for Basis Library compatibility
|
file |
diff |
annotate
|
| Thu, 14 Nov 1996 16:01:36 +0100 |
nipkow |
Modified formal of thms in html file.
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 11:11:22 +0200 |
paulson |
Changed freeze to freeze_thaw
|
file |
diff |
annotate
|
| Tue, 30 Apr 1996 12:40:09 +0200 |
clasohm |
changed use_thy's behaviour so that if the user specifies a path for a theory
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 12:38:16 +0200 |
clasohm |
use_dir and exit_use_dir now change the CWD only temporarily
|
file |
diff |
annotate
|
| Fri, 19 Apr 1996 11:10:26 +0200 |
clasohm |
added thyname_of_sign (used in HOL/thy_data.ML)
|
file |
diff |
annotate
|
| Fri, 12 Apr 1996 12:41:59 +0200 |
clasohm |
add_thydata and get_thydata now take a string as their first argument
|
file |
diff |
annotate
|
| Thu, 11 Apr 1996 13:41:22 +0200 |
clasohm |
fixed bug in set_current_thy
|
file |
diff |
annotate
|
| Sun, 24 Mar 1996 18:36:28 +0100 |
clasohm |
moved init_data to new public function set_current_thy
|
file |
diff |
annotate
|
| Fri, 22 Mar 1996 12:06:08 +0100 |
clasohm |
fixed incompatibility of add_to_parents with SML109's new Io exceptions
|
file |
diff |
annotate
|
| Thu, 21 Mar 1996 11:09:47 +0100 |
paulson |
For the new version of name_thm. Now the same theorem
|
file |
diff |
annotate
|
| Wed, 20 Mar 1996 13:21:12 +0100 |
clasohm |
added warning and automatic deactivation of HTML generation if we cannot write
|
file |
diff |
annotate
|
| Fri, 15 Mar 1996 12:01:19 +0100 |
berghofe |
Added some functions which allow redirection of Isabelle's output
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 14:10:44 +0100 |
clasohm |
moved part of delete_thms into init_thyinfo
|
file |
diff |
annotate
|
| Tue, 05 Mar 1996 13:18:58 +0100 |
clasohm |
added function "section" for HTML section headings
|
file |
diff |
annotate
|
| Mon, 04 Mar 1996 12:28:48 +0100 |
clasohm |
made delete_thms public
|
file |
diff |
annotate
|
| Fri, 01 Mar 1996 10:19:51 +0100 |
paulson |
Addition of proof objects
|
file |
diff |
annotate
|
| Mon, 19 Feb 1996 13:54:15 +0100 |
clasohm |
fixed bug in init_data (put was only invoked for the first date)
|
file |
diff |
annotate
|
| Thu, 08 Feb 1996 12:26:16 +0100 |
clasohm |
simplified bind_thm
|
file |
diff |
annotate
|
| Tue, 06 Feb 1996 12:44:31 +0100 |
clasohm |
made Isabelle compatible with SML/NJ 1.09
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:50:10 +0100 |
clasohm |
added facility to associate arbitrary data with theories
|
file |
diff |
annotate
|
| Mon, 18 Dec 1995 13:02:45 +0100 |
clasohm |
added automatic handling of wrongly set base_path
|
file |
diff |
annotate
|
| Fri, 15 Dec 1995 12:15:39 +0100 |
clasohm |
init_html now makes sure that base_path contains a physical path and no
|
file |
diff |
annotate
|
| Wed, 13 Dec 1995 14:14:06 +0100 |
clasohm |
renamed parents_of to parents_of_name to avoid name clash with function
|
file |
diff |
annotate
|
| Wed, 06 Dec 1995 14:53:55 +0100 |
clasohm |
fixed bug: cur_thyname was overwritten because of early assignment
|
file |
diff |
annotate
|
| Fri, 01 Dec 1995 12:24:06 +0100 |
clasohm |
removed debugging message;
|
file |
diff |
annotate
|
| Mon, 27 Nov 1995 13:37:13 +0100 |
clasohm |
renamed make_chart to finish_html
|
file |
diff |
annotate
|
| Tue, 21 Nov 1995 14:50:37 +0100 |
clasohm |
added functions for storing and retrieving information about datatypes
|
file |
diff |
annotate
|
| Tue, 21 Nov 1995 12:36:31 +0100 |
clasohm |
index.html files are now made separatly for each subdirectory
|
file |
diff |
annotate
|
| Wed, 15 Nov 1995 13:28:21 +0100 |
clasohm |
added link to README.html or README
|
file |
diff |
annotate
|
| 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
|