src/HOL/Extraction.thy
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.