src/HOL/Extraction.thy
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-05-03 nipkow 2015-05-03 swap False to the right in assumptions to be eliminated at the right end
2015-04-28 nipkow 2015-04-28 undid 6d7b7a037e8d
2015-04-25 nipkow 2015-04-25 new ==> simp rule
2015-04-14 nipkow 2015-04-14 prepared for more meta-simp rules (by Stefan Berghofer)
2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-15 blanchet 2014-09-15 'code' is needed for extraction datatype
2014-09-15 blanchet 2014-09-15 generate 'code' attribute only if 'code' plugin is enabled
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new'
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-12 blanchet 2014-02-12 transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
2013-06-30 wenzelm 2013-06-30 just one alternative proof syntax, which also works for Proof_Syntax.pretty_proof/Proof_Syntax.read_proof roundtrip;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2010-06-01 berghofe 2010-06-01 Adapted to new format of proof terms containing explicit proofs of class membership.
2010-01-10 berghofe 2010-01-10 Expand proofs of induct_atomize'/rulify'.
2009-11-17 wenzelm 2009-11-17 eliminated dead code;
2009-11-15 wenzelm 2009-11-15 add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature; explicit extraction_expand vs. extraction_expand_def attribute;
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.