src/HOL/ex/svc_funcs.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-05-12 wenzelm 2013-05-12 decentralized historic settings;
2011-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2011-07-16 wenzelm 2011-07-16 moved bash operations to Isabelle_System (cf. Scala version);
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
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;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-06 wenzelm 2008-03-06 replaced execute by system_out;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-09-15 haftmann 2007-09-15 fixed title
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-13 haftmann 2006-12-13 introduced mk/dest_numeral/number for mk/dest_binum etc.
2006-11-16 wenzelm 2006-11-16 moved some fundamental concepts to General/basics.ML;
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-04 haftmann 2006-10-04 *** empty log message ***
2006-03-31 paulson 2006-03-31 removed some illegal characters: they were crashing SML/NJ
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2005-09-17 wenzelm 2005-09-17 removed obsolete BasisLibrary;
2005-07-14 wenzelm 2005-07-14 improved oracle setup;
2005-06-05 wenzelm 2005-06-05 File.shell_path;
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
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.
2004-06-21 wenzelm 2004-06-21 File.quote_sysify_path;
2002-02-05 wenzelm 2002-02-05 moved SVC stuff to ex;