1997-08-06 berghofe 1997-08-06 Added function "file_exists".
1997-08-06 berghofe 1997-08-06 Removed function file_exists (now included in library.ML)
1997-08-06 berghofe 1997-08-06 Moved functions for theory information storage / retrieval from thy_read.ML to thy_info.ML .
1997-08-06 berghofe 1997-08-06 This file now contains all functions for generating html and graph data.
1997-08-06 berghofe 1997-08-06 Moved several functions: html generation --> browser_info.ML theory information storage / retrieval --> thy_info.ML theorem storage (qed) --> thm_database.ML
1997-08-06 berghofe 1997-08-06 Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
1997-08-06 berghofe 1997-08-06 Added some additional "use" commands for new files (browser_info.ML and thy_info.ML)
1997-08-06 berghofe 1997-08-06 Source files for Isabelle theory graph browser. Initial revision.
1997-08-06 berghofe 1997-08-06 Makefile for GraphBrowser Initial revision
1997-08-05 wenzelm 1997-08-05 added getenv;
1997-08-05 wenzelm 1997-08-05 removed smlnj-1.07;
1997-08-05 wenzelm 1997-08-05 cleaned up; added getenv;
1997-08-05 wenzelm 1997-08-05 tuned comments;
1997-08-05 wenzelm 1997-08-05 removed ML-Systems/smlnj-1.07.ML;
1997-08-05 wenzelm 1997-08-05 SML/NJ 1.07 no longer supported!
1997-08-05 wenzelm 1997-08-05 cleaned up; added getenv;
1997-08-05 nipkow 1997-08-05 Added example mapf which requires a special congruence rule.
1997-08-05 nipkow 1997-08-05 Added function `replicate' and lemmas map_cong and set_replicate.
1997-08-05 wenzelm 1997-08-05 cleaned up; added getenv;
1997-08-05 paulson 1997-08-05 Corrected a comment
1997-08-04 nipkow 1997-08-04 Added a take/dropWhile lemma.
1997-08-01 nipkow 1997-08-01 Generalized nth_drop (Conny).
1997-08-01 nipkow 1997-08-01 Corected bug in def of dropWhile (also present in Haskell lib!)
1997-08-01 nipkow 1997-08-01 Had to remove {x.x=a} = a from !simpset in one proof.
1997-08-01 nipkow 1997-08-01 Added {x.x=a} = a to !simpset.
1997-07-25 wenzelm 1997-07-25 removed split_paired_Ex; fixed proc args;
1997-07-25 nipkow 1997-07-25 new simproc
1997-07-25 wenzelm 1997-07-25 *** empty log message ***
1997-07-25 wenzelm 1997-07-25 load simplifier.ML (again);
1997-07-25 wenzelm 1997-07-25 added prems argument to simplification procedures;
1997-07-25 wenzelm 1997-07-25 remove references to simplifier.ML;
1997-07-25 wenzelm 1997-07-25 improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-24 nipkow 1997-07-24 Added a few lemmas.
1997-07-24 nipkow 1997-07-24 Deleted comment.
1997-07-24 nipkow 1997-07-24 Replaced clumsy rewriting by the new function simplify on thms.
1997-07-24 nipkow 1997-07-24 List.ML: added lemmas by Stefan Merz. simpodata.ML: removed rules about ? now subsumed by simplification proc.
1997-07-24 paulson 1997-07-24 set_of_list -> set
1997-07-23 nipkow 1997-07-23 Simplified a few proofs because of improved simplification.
1997-07-23 nipkow 1997-07-23 Prod.ML: Added split_paired_EX and lots of comments about failed attempts to automate reasoning about products. simpdata.ML: added simplification procedure for simplifying existential statements of the form ? x. ... & x = t & ...
1997-07-23 wenzelm 1997-07-23 added simplification meta rules;
1997-07-23 wenzelm 1997-07-23 standard congs;
1997-07-23 paulson 1997-07-23 Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.
1997-07-23 paulson 1997-07-23 Now Datatype.occs_in_prems prints the necessary warning ITSELF. It is also easier to invoke and even works if the induction variable is a parameter (rather than a free variable).
1997-07-23 paulson 1997-07-23 Uses new version of Datatype.occs_in_prems
1997-07-23 paulson 1997-07-23 auto update
1997-07-23 paulson 1997-07-23 Removal of tactical STATE
1997-07-23 wenzelm 1997-07-23 fixed polymorphic val;
1997-07-23 wenzelm 1997-07-23 tuned congs: standard;
1997-07-23 wenzelm 1997-07-23 improved simp tracing;
1997-07-23 wenzelm 1997-07-23 added simplification meta rules;
1997-07-23 wenzelm 1997-07-23 tmp fix to accomodate rep_ss changes;
1997-07-23 wenzelm 1997-07-23 added rewrite_thm;
1997-07-23 wenzelm 1997-07-23 tuned apsome;
1997-07-22 wenzelm 1997-07-22 added error_msg;
1997-07-22 wenzelm 1997-07-22 tuned error / warning;
1997-07-22 wenzelm 1997-07-22 added print_ss; improved merge;
1997-07-22 wenzelm 1997-07-22 added dest_mss, merge_mss; fixed matching of simproc lhss;
1997-07-22 wenzelm 1997-07-22 tuned title;
1997-07-22 wenzelm 1997-07-22 added dest and merge operations;
1997-07-22 wenzelm 1997-07-22 added pretty_cterm;