src/HOL/IsaMakefile
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-18 wenzelm 2007-09-18 moved Tools/integer.ML to Pure/General/integer.ML;
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-09-18 haftmann 2007-09-18 separated code for inductive sequences from inductive_codegen.ML
2007-09-18 nipkow 2007-09-18 sorting
2007-09-16 wenzelm 2007-09-16 added Induct/Common_Patterns.thy;
2007-09-06 berghofe 2007-09-06 - New theories Lambda/NormalForm and Lambda/Standardization - Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories
2007-08-29 wenzelm 2007-08-29 added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
2007-08-29 wenzelm 2007-08-29 removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
2007-08-28 huffman 2007-08-28 revert to Word library version from 2007/08/20
2007-08-28 berghofe 2007-08-28 codegen.ML is now loaded in Pure again.
2007-08-28 huffman 2007-08-28 HOL-Word-Examples
2007-08-23 huffman 2007-08-23 Word/BinInduct.thy
2007-08-22 huffman 2007-08-22 removed Word/Size.thy; replaced len_of TYPE('a) with CARD('a); replaced axclass len with class finite; replaced axclass len0 with class type
2007-08-22 huffman 2007-08-22 Word/WordBoolList.thy
2007-08-21 wenzelm 2007-08-21 use HOL-ex later;
2007-08-20 huffman 2007-08-20 Word/document/root.tex
2007-08-20 kleing 2007-08-20 * HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution
2007-08-20 kleing 2007-08-20 boolean algebras as locales and numbers as types by Brian Huffman
2007-08-18 wenzelm 2007-08-18 converted ex/MT.ML;
2007-08-18 wenzelm 2007-08-18 make HOL-ex earlier;
2007-08-15 paulson 2007-08-15 combining the relevance filter with res_atp
2007-08-15 haftmann 2007-08-15 updated code generator setup
2007-08-09 haftmann 2007-08-09 re-eliminated Option.thy
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-08-03 wenzelm 2007-08-03 reactivated Nominal/Examples/Class.thy;
2007-08-03 wenzelm 2007-08-03 added dependency on Tools/Metis/metis.ML;
2007-08-02 wenzelm 2007-08-02 converted Meson tests to proper theory;
2007-07-31 wenzelm 2007-07-31 removed obsolete HOL/Real/ROOT.ML;
2007-07-31 wenzelm 2007-07-31 added Tools/lin_arith.ML;
2007-07-31 chaieb 2007-07-31 Added dependency on langford files in Tools/Qelim
2007-07-29 wenzelm 2007-07-29 removed obsolete Tools/res_atpset.ML;
2007-07-20 haftmann 2007-07-20 dropped Nat.ML legacy bindings
2007-07-19 haftmann 2007-07-19 uniform naming conventions for CG theories
2007-07-11 obua 2007-07-11 changed sources for HOL-Complex-Matrix
2007-07-11 berghofe 2007-07-11 Added new package for inductive sets.
2007-07-09 wenzelm 2007-07-09 HOL-Complex-Matrix: fixed deps -- sort of;
2007-07-05 wenzelm 2007-07-05 added Tools/numeral.ML;
2007-07-03 chaieb 2007-07-03 Dependency on reflection_data.ML to build HOL-ex
2007-06-29 paulson 2007-06-29 bug fixes to proof reconstruction
2007-06-26 nipkow 2007-06-26 added NBE
2007-06-25 krauss 2007-06-25 removed "sum_tools.ML" in favour of BalancedTree
2007-06-21 wenzelm 2007-06-21 moved quantifier elimination tools to Tools/Qelim/;
2007-06-21 wenzelm 2007-06-21 renamed NatSimprocs.thy to Arith_Tools.thy; incorporated HOL/Presburger.thy into NatSimprocs.thy;
2007-06-21 wenzelm 2007-06-21 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
2007-06-21 paulson 2007-06-21 integration of Metis prover
2007-06-20 wenzelm 2007-06-20 added Tools/metis_tools.ML;
2007-06-11 chaieb 2007-06-11 Added dependency on file Groebner_Basis.thy
2007-06-11 chaieb 2007-06-11 Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
2007-06-06 urbanc 2007-06-06 take out Class.thy again, because it does not yet compile cleanly
2007-06-06 chaieb 2007-06-06 New Reflected Presburger added to HOL/ex
2007-06-05 wenzelm 2007-06-05 added ex/Groebner_Examples.thy; renamed ex/Eval_Examples.thy;
2007-06-05 chaieb 2007-06-05 Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
2007-06-05 wenzelm 2007-06-05 Semiring normalization and Groebner Bases.
2007-06-05 haftmann 2007-06-05 merged Code_Generator.thy into HOL.thy
2007-06-05 urbanc 2007-06-05 included Class.thy in the compiling process for Nominal/Examples
2007-06-03 wenzelm 2007-06-03 HOL-ex: tuned deps;
2007-06-01 webertj 2007-06-01 tuned
2007-06-01 webertj 2007-06-01 some tests for arith added
2007-06-01 nipkow 2007-06-01 Moved list comprehension into List