src/HOL/Modelcheck/mucke_oracle.ML
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-02-06 ago renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2009-11-24 ago curried take/drop
2009-10-19 ago always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-24 ago do not open OldGoals;
2009-07-24 ago explicit OldGoals;
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-20 ago eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-09-18 ago simplified oracle interface;
2008-06-18 ago OldGoals.simple_read_term;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-03-20 ago simplified get_thm(s): back to plain name argument;
2008-03-19 ago more antiquotations;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-06 ago replaced execute by system_out;
2007-09-18 ago simplified PrintMode interfaces;
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 ago rep_thm/cterm/ctyp: removed obsolete sign field;
2006-07-25 ago renamed Term.variant_abs to Syntax.variant_abs;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2005-12-20 ago removed superfluos is_prefix functions
2005-10-21 ago OldGoals;
2005-09-14 ago introduces AList.lookup
2005-09-06 ago converted to Isar theory format;
2005-06-28 ago Constant "If" is now local
2005-06-20 ago get_thm(s): Name;
2005-06-17 ago replaced obsolete theory_of_sign by theory_of_thm;
2005-06-05 ago File.shell_path;
2005-05-31 ago no_tac;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Adapted to modified interface of PureThy.get_thm(s).
2004-06-21 ago File.quote_sysify_path;
2004-06-20 ago got rid of Output.output for default print mode;
2004-05-29 ago Output.output;
1999-08-20 ago mucke -res;
1999-08-19 ago quite a lot of tuning an cleanup;
1999-04-22 ago fixed IO;
1999-04-22 ago added for mucke translation;