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