src/HOL/ex/SVC_Oracle.thy
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-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
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-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-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-17 wenzelm 2008-09-17 moved global ML bindings to global place;
2008-01-21 haftmann 2008-01-21 avoiding direct references to numeral presentation
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-08-29 wenzelm 2007-08-29 removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
2006-10-01 wenzelm 2006-10-01 proper use of svc_oracle.ML;
2005-09-14 wenzelm 2005-09-14 tuned headers etc.;
2005-07-14 wenzelm 2005-07-14 improved oracle setup;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-02-05 wenzelm 2002-02-05 moved SVC stuff to ex;