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