src/Pure/Proof/extraction.ML
2005-09-02 haftmann 2005-09-02 some 'assoc' etc. refactoring
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; tuned;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-01 wenzelm 2005-08-01 replaced atless by term_ord;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms; tuned assoc;
2005-07-13 wenzelm 2005-07-13 improved Net interface;
2005-07-13 haftmann 2005-07-13 (fix for an accidental commit)
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-11 wenzelm 2005-06-11 renamed Sign.intern_tycon to Sign.intern_type;
2005-06-09 wenzelm 2005-06-09 can (Thm.get_axiom_i thy) name; removed duplicate code;
2005-06-05 wenzelm 2005-06-05 Type.freeze;
2005-06-02 wenzelm 2005-06-02 tuned;
2005-05-31 wenzelm 2005-05-31 Theory.restore_naming; tuned fold;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-12-10 berghofe 2004-12-10 Added term cache to function condrew in order to speed up rewriting.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-03-19 paulson 2004-03-19 Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.
2003-01-29 berghofe 2003-01-29 Fixed bug in function corr.
2002-11-27 berghofe 2002-11-27 Correctness proofs are now modular, too.
2002-11-17 berghofe 2002-11-17 Fixed small bug that caused some definitions to be "forgotten".
2002-11-13 berghofe 2002-11-13 - exported functions etype_of and mk_typ - new function realizes_of
2002-09-30 berghofe 2002-09-30 Added check for axioms with "realizes Null A = A".
2002-07-24 berghofe 2002-07-24 Tuned type constraint of function merge_rules to make smlnj happy.
2002-07-21 berghofe 2002-07-21 Added program extraction module.