src/HOL/PreList.thy
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-18 paulson 2007-09-18 metis now available in PreList
2007-09-18 nipkow 2007-09-18 sorting
2007-07-10 haftmann 2007-07-10 clarified import
2007-06-21 wenzelm 2007-06-21 moved Presburger setup back to Presburger.thy;
2007-06-21 wenzelm 2007-06-21 renamed NatSimprocs.thy to Arith_Tools.thy; incorporated HOL/Presburger.thy into NatSimprocs.thy;
2007-05-06 haftmann 2007-05-06 PreList imports RecDef
2006-11-22 haftmann 2006-11-22 does not import Hilber_Choice any longer
2006-11-13 haftmann 2006-11-13 PreList = Main - List
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-09-19 haftmann 2006-09-19 text cleanup
2005-09-20 wenzelm 2005-09-20 tuned theory dependencies;
2005-08-09 nipkow 2005-08-09 moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
2005-07-08 nipkow 2005-07-08 changed imports due to new GCD.thy
2004-11-19 chaieb 2004-11-19 Barith removed VS: ----------------------------------------------------------------------
2004-10-06 chaieb 2004-10-06 changed in order to insert Barith.thy
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2003-07-24 paulson 2003-07-24 tidied
2003-03-25 berghofe 2003-03-25 Added Presburger theory.
2002-07-04 wenzelm 2002-07-04 tuned;
2002-02-21 wenzelm 2002-02-21 removed theory Option;
2002-02-05 wenzelm 2002-02-05 moved SVC stuff to ex;
2001-12-06 wenzelm 2001-12-06 less_induct, wf_induct_rule;
2001-11-28 wenzelm 2001-11-28 tuned declarations;
2001-11-02 wenzelm 2001-11-02 theory Calculation move to Set;
2001-10-27 wenzelm 2001-10-27 moved product cases/induct to theory Datatype;
2001-10-16 wenzelm 2001-10-16 tuned;
2001-10-15 kleing 2001-10-15 canonical 'cases'/'induct' rules for n-tuples (n=3..7) (really belongs to theory Product_Type, but doesn't work there yet)
2000-12-23 wenzelm 2000-12-23 hide type node item;
2000-12-15 wenzelm 2000-12-15 tuned comment;
2000-12-14 wenzelm 2000-12-14 added Summation;
2000-11-24 nipkow 2000-11-24 hide many names from Datatype_Universe.
2000-10-18 wenzelm 2000-10-18 tuned declarations;
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-08-17 wenzelm 2000-08-17 fixed deps;
2000-06-14 wenzelm 2000-06-14 theorems [cases type: bool] = case_split;
2000-05-12 paulson 2000-05-12 NatSimprocs is now a theory, not a file
2000-05-08 wenzelm 2000-05-08 moved theory Sexp to Induct examples;
2000-04-21 paulson 2000-04-21 new file Integ/NatSimprocs.ML
2000-03-24 nipkow 2000-03-24 comments
2000-03-16 wenzelm 2000-03-16 added HOL/PreLIst.thy;