src/Pure/Thy/thy_read.ML
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
1994-06-17 clasohm 1994-06-17 replaced "foldl merge_theories" by "merge_thy_list" in base_on