src/Pure/Thy/thy_read.ML
1997-04-24 nipkow 1997-04-24 get_thydata accesses the second component of the data field. This component used to be empty until set at the end of loading an ML file. Now the second component is already set when the thy file has ben read.
1996-12-16 wenzelm 1996-12-16 now uses SymbolInput.use;
1996-11-27 paulson 1996-11-27 Converted I/O operatios for Basis Library compatibility
1996-11-14 nipkow 1996-11-14 Modified formal of thms in html file.
1996-09-26 paulson 1996-09-26 Changed freeze to freeze_thaw
1996-04-30 clasohm 1996-04-30 changed use_thy's behaviour so that if the user specifies a path for a theory the loadpath is temporarily expanded while the ancestors are loaded
1996-04-23 clasohm 1996-04-23 use_dir and exit_use_dir now change the CWD only temporarily
1996-04-19 clasohm 1996-04-19 added thyname_of_sign (used in HOL/thy_data.ML)
1996-04-12 clasohm 1996-04-12 add_thydata and get_thydata now take a string as their first argument
1996-04-11 clasohm 1996-04-11 fixed bug in set_current_thy
1996-03-24 clasohm 1996-03-24 moved init_data to new public function set_current_thy
1996-03-22 clasohm 1996-03-22 fixed incompatibility of add_to_parents with SML109's new Io exceptions
1996-03-21 paulson 1996-03-21 For the new version of name_thm. Now the same theorem is stored as is returned, as both contain a label and a link to the previous derivation. So get_thm no longer needs to attach a label to its resulting theorem.
1996-03-20 clasohm 1996-03-20 added warning and automatic deactivation of HTML generation if we cannot write .theory_list.txt; fixed bug which occured when index_path's value is "/"
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-06 clasohm 1996-03-06 moved part of delete_thms into init_thyinfo
1996-03-05 clasohm 1996-03-05 added function "section" for HTML section headings
1996-03-04 clasohm 1996-03-04 made delete_thms public
1996-03-01 paulson 1996-03-01 Addition of proof objects
1996-02-19 clasohm 1996-02-19 fixed bug in init_data (put was only invoked for the first date)
1996-02-08 clasohm 1996-02-08 simplified bind_thm
1996-02-06 clasohm 1996-02-06 made Isabelle compatible with SML/NJ 1.09
1996-01-29 clasohm 1996-01-29 added facility to associate arbitrary data with theories
1995-12-18 clasohm 1995-12-18 added automatic handling of wrongly set base_path
1995-12-15 clasohm 1995-12-15 init_html now makes sure that base_path contains a physical path and no symbolic links
1995-12-13 clasohm 1995-12-13 renamed parents_of to parents_of_name to avoid name clash with function from thm.ML
1995-12-06 clasohm 1995-12-06 fixed bug: cur_thyname was overwritten because of early assignment
1995-12-01 clasohm 1995-12-01 removed debugging message; link to non-existing super index is now omitted silently
1995-11-27 clasohm 1995-11-27 renamed make_chart to finish_html
1995-11-21 clasohm 1995-11-21 added functions for storing and retrieving information about datatypes
1995-11-21 clasohm 1995-11-21 index.html files are now made separatly for each subdirectory
1995-11-15 clasohm 1995-11-15 added link to README.html or README
1995-11-07 clasohm 1995-11-07 added leading "." to HTML filenames
1995-11-03 clasohm 1995-11-03 removed image borders from index.html files
1995-11-02 clasohm 1995-11-02 removed borders from images in charts; replaced green arrow by "..."
1995-10-26 clasohm 1995-10-26 renamed chart00 and 00-chart to "index"
1995-10-25 clasohm 1995-10-25 removed "duplicate" warning from store_thm_db; changed place where store_thm_db is called for a theory's axioms
1995-10-24 clasohm 1995-10-24 added generation of HTML files to thy_read.ML; removed old HTML package
1995-10-04 clasohm 1995-10-04 added removal of theorems if theory is to be reloaded; changed functions for local simpsets
1995-09-01 clasohm 1995-09-01 restored old invocation of use_string till I can make the new version work
1995-09-01 clasohm 1995-09-01 added cleanup of global simpset to thy_read; replaced error by warning for duplicate names in theorem database
1995-08-30 clasohm 1995-08-30 added check for duplicate theorems in theorem database; changed warnings and error messages in thy_read to distinguish between theorems in theor_y_ database and in theor_em_ database
1995-08-08 nipkow 1995-08-08 corrected bind_thm: now applies "standard" uniformly.
1995-06-23 clasohm 1995-06-23 added a few comments on ThyInfo
1995-06-22 clasohm 1995-06-22 changed call of store_thm_db so that it's result is not displayed by PolyML or SML
1995-05-29 clasohm 1995-05-29 added theorem database which contains axioms and theorems indexed by the constants they contain
1995-05-03 clasohm 1995-05-03 fixed bug in thy_unchanged that occurred when the .thy file was changed but the .ML file hadn't been read before; tmpfile is now deleted immediatly after reading the .thy file in use_thy
1995-03-23 clasohm 1995-03-23 fixed bug: parent theory wasn't loaded if .thy file was completly read before (regardless of the .ML file)
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-01-23 clasohm 1995-01-23 simplified get_thm a bit
1994-12-14 clasohm 1994-12-14 changed get_thm to search all parent theories if the theorem is not found in the current theory
1994-12-12 wenzelm 1994-12-12 added print_theory that prints stored thms;
1994-12-09 clasohm 1994-12-09 added warning for already stored theorem to store_thm
1994-12-07 clasohm 1994-12-07 moved first call of store_theory from thy_read.ML to created .thy.ML file
1994-12-06 clasohm 1994-12-06 added bind_thm
1994-11-25 clasohm 1994-11-25 added qed_goal[w]
1994-11-18 clasohm 1994-11-18 added call of store_theory after thy file has been read
1994-09-06 clasohm 1994-09-06 renamed base_on into mk_base and moved it to the beginning of the generated .thy.ML file to make sure that all base theories are present when ML executes the rest of this file
1994-08-19 wenzelm 1994-08-19 added theory_of_sign, theory_of_thm; renamed get_thms to thms_of; improved store_thms etc.;
1994-07-15 clasohm 1994-07-15 added check for concistency of filename and theory name; made loaded_thys a symtab instead of an association list; added store_thm, qed, get_thm, get_thms