src/HOL/Plain.thy
2011-03-03 wenzelm 2011-03-03 discontinued legacy load path;
2010-12-29 wenzelm 2010-12-29 theory loader: implicit load path is considered legacy;
2010-10-26 blanchet 2010-10-26 reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-25 haftmann 2010-10-25 moved sledgehammer to Plain; tuned dependencies
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-10-04 blanchet 2010-10-04 move Meson to Plain
2010-08-12 haftmann 2010-08-12 group record-related ML files
2009-11-10 haftmann 2009-11-10 tuned imports
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-03-06 haftmann 2009-03-06 moved instance option :: finite to Option.thy
2009-02-23 huffman 2009-02-23 change imports to move Fact.thy outside Plain
2009-02-09 chaieb 2009-02-09 Now imports Fact as suggested by Florian in order to avoid the typerep problem
2009-02-06 blanchet 2009-02-06 Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.
2009-01-21 haftmann 2009-01-21 changed import hierarchy
2009-01-02 wenzelm 2009-01-02 tuned header and description of boot files;
2008-06-26 haftmann 2008-06-26 established Plain theory and image