src/HOL/ex/svc_funcs.ML
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;