src/Pure/Thy/thy_read.ML
Fri, 18 Jul 1997 13:35:36 +0200 wenzelm tuned warning;
Thu, 24 Apr 1997 18:03:23 +0200 nipkow get_thydata accesses the second component of the data field. This component
Mon, 16 Dec 1996 10:03:30 +0100 wenzelm now uses SymbolInput.use;
Wed, 27 Nov 1996 10:54:16 +0100 paulson Converted I/O operatios for Basis Library compatibility
Thu, 14 Nov 1996 16:01:36 +0100 nipkow Modified formal of thms in html file.
Thu, 26 Sep 1996 11:11:22 +0200 paulson Changed freeze to freeze_thaw
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
Tue, 23 Apr 1996 12:38:16 +0200 clasohm use_dir and exit_use_dir now change the CWD only temporarily
Fri, 19 Apr 1996 11:10:26 +0200 clasohm added thyname_of_sign (used in HOL/thy_data.ML)
Fri, 12 Apr 1996 12:41:59 +0200 clasohm add_thydata and get_thydata now take a string as their first argument
Thu, 11 Apr 1996 13:41:22 +0200 clasohm fixed bug in set_current_thy
Sun, 24 Mar 1996 18:36:28 +0100 clasohm moved init_data to new public function set_current_thy
Fri, 22 Mar 1996 12:06:08 +0100 clasohm fixed incompatibility of add_to_parents with SML109's new Io exceptions
Thu, 21 Mar 1996 11:09:47 +0100 paulson For the new version of name_thm. Now the same theorem
Wed, 20 Mar 1996 13:21:12 +0100 clasohm added warning and automatic deactivation of HTML generation if we cannot write
Fri, 15 Mar 1996 12:01:19 +0100 berghofe Added some functions which allow redirection of Isabelle's output
Wed, 06 Mar 1996 14:10:44 +0100 clasohm moved part of delete_thms into init_thyinfo
Tue, 05 Mar 1996 13:18:58 +0100 clasohm added function "section" for HTML section headings
Mon, 04 Mar 1996 12:28:48 +0100 clasohm made delete_thms public
Fri, 01 Mar 1996 10:19:51 +0100 paulson Addition of proof objects
Mon, 19 Feb 1996 13:54:15 +0100 clasohm fixed bug in init_data (put was only invoked for the first date)
Thu, 08 Feb 1996 12:26:16 +0100 clasohm simplified bind_thm
Tue, 06 Feb 1996 12:44:31 +0100 clasohm made Isabelle compatible with SML/NJ 1.09
Mon, 29 Jan 1996 13:50:10 +0100 clasohm added facility to associate arbitrary data with theories
Mon, 18 Dec 1995 13:02:45 +0100 clasohm added automatic handling of wrongly set base_path
Fri, 15 Dec 1995 12:15:39 +0100 clasohm init_html now makes sure that base_path contains a physical path and no
Wed, 13 Dec 1995 14:14:06 +0100 clasohm renamed parents_of to parents_of_name to avoid name clash with function
Wed, 06 Dec 1995 14:53:55 +0100 clasohm fixed bug: cur_thyname was overwritten because of early assignment
Fri, 01 Dec 1995 12:24:06 +0100 clasohm removed debugging message;
Mon, 27 Nov 1995 13:37:13 +0100 clasohm renamed make_chart to finish_html
Tue, 21 Nov 1995 14:50:37 +0100 clasohm added functions for storing and retrieving information about datatypes
Tue, 21 Nov 1995 12:36:31 +0100 clasohm index.html files are now made separatly for each subdirectory
Wed, 15 Nov 1995 13:28:21 +0100 clasohm added link to README.html or README
Tue, 07 Nov 1995 13:15:04 +0100 clasohm added leading "." to HTML filenames
Fri, 03 Nov 1995 12:00:46 +0100 clasohm removed image borders from index.html files
Thu, 02 Nov 1995 14:16:00 +0100 clasohm removed borders from images in charts;
Thu, 26 Oct 1995 13:53:04 +0100 clasohm renamed chart00 and 00-chart to "index"
Wed, 25 Oct 1995 13:41:45 +0100 clasohm removed "duplicate" warning from store_thm_db;
Tue, 24 Oct 1995 13:53:09 +0100 clasohm added generation of HTML files to thy_read.ML;
Wed, 04 Oct 1995 12:59:52 +0100 clasohm added removal of theorems if theory is to be reloaded; changed functions for
Fri, 01 Sep 1995 13:51:49 +0200 clasohm restored old invocation of use_string till I can make the new version work
Fri, 01 Sep 1995 13:28:54 +0200 clasohm added cleanup of global simpset to thy_read;
Wed, 30 Aug 1995 14:04:39 +0200 clasohm added check for duplicate theorems in theorem database;
Tue, 08 Aug 1995 09:27:02 +0200 nipkow corrected bind_thm: now applies "standard" uniformly.
Fri, 23 Jun 1995 11:59:06 +0200 clasohm added a few comments on ThyInfo
Thu, 22 Jun 1995 12:58:39 +0200 clasohm changed call of store_thm_db so that it's result is not displayed
Mon, 29 May 1995 13:55:06 +0200 clasohm added theorem database which contains axioms and theorems indexed by the
Wed, 03 May 1995 15:25:30 +0200 clasohm fixed bug in thy_unchanged that occurred when the .thy file was changed
Thu, 23 Mar 1995 15:39:13 +0100 clasohm fixed bug: parent theory wasn't loaded if .thy file was completly read before
Fri, 03 Mar 1995 11:48:05 +0100 clasohm added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
Mon, 23 Jan 1995 12:20:10 +0100 clasohm simplified get_thm a bit
Wed, 14 Dec 1994 13:03:09 +0100 clasohm changed get_thm to search all parent theories if the theorem is not found
Mon, 12 Dec 1994 10:26:05 +0100 wenzelm added print_theory that prints stored thms;
Fri, 09 Dec 1994 13:05:03 +0100 clasohm added warning for already stored theorem to store_thm
Wed, 07 Dec 1994 12:34:47 +0100 clasohm moved first call of store_theory from thy_read.ML to created .thy.ML file
Tue, 06 Dec 1994 12:50:13 +0100 clasohm added bind_thm
Fri, 25 Nov 1994 09:13:49 +0100 clasohm added qed_goal[w]
Fri, 18 Nov 1994 13:08:10 +0100 clasohm added call of store_theory after thy file has been read
Tue, 06 Sep 1994 14:44:10 +0200 clasohm renamed base_on into mk_base and moved it to the beginning of the generated
Fri, 19 Aug 1994 15:39:19 +0200 wenzelm added theory_of_sign, theory_of_thm;
less more (0) -60 tip