isabelle: File revisions

src/HOL/Extraction.thy

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

isabelle

RSS Atom