src/HOL/Extraction.thy
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2009-02-16 berghofe 2009-02-16 Adapted to encoding of sets as predicates.
2008-11-15 wenzelm 2008-11-15 rewrite_proof: simplified simprocs (no name required);
2008-08-24 haftmann 2008-08-24 default replaces arbitrary
2007-11-13 berghofe 2007-11-13 Added TrueE to extraction_expand.
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-02-07 berghofe 2007-02-07 Added meta_spec to extraction_expand.
2006-10-10 haftmann 2006-10-10 added eq_True eq_False True_implies_equals to extraction_expand
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-23 wenzelm 2005-12-23 removed obsolete induct_atomize_old;
2005-12-22 wenzelm 2005-12-22 updated auxiliary facts for induct method;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-31 wenzelm 2005-05-31 tuned;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-12-10 berghofe 2004-12-10 Realizer for exE now uses let instead of case.
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-08-27 skalberg 2003-08-27 Prepared for extended identifiers (\<alpha>, etc.)
2003-05-01 berghofe 2003-05-01 induct_impliesI is now unfolded.
2003-04-23 berghofe 2003-04-23 Tuned realizer for exE rule, to avoid blowup of extracted program.
2002-11-27 berghofe 2002-11-27 Changed format of realizers / correctness proofs.
2002-09-30 berghofe 2002-09-30 Added elim_vars to preprocessor.
2002-08-07 berghofe 2002-08-07 Removed (now unneeded) declaration of realizers for induction on natural numbers.
2002-08-05 berghofe 2002-08-05 Removed reference to theory NatDef.
2002-07-21 berghofe 2002-07-21 Added theory for setting up program extraction.