src/HOL/Statespace/state_space.ML
2011-03-22 wenzelm 2011-03-22 statespace syntax: strip positions -- type constraints are unexpected here;
2011-01-16 wenzelm 2011-01-16 added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-18 ballarin 2010-12-18 Add mixins to sublocale command.
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 wenzelm 2010-08-27 eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; modernized attribute setup;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
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-08-12 haftmann 2010-08-12 Named_Target.init: empty string represents theory target
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-17 wenzelm 2010-05-17 tuned;
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-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-29 wenzelm 2010-04-29 adapted ProofContext.infer_type;
2010-04-15 wenzelm 2010-04-15 inline old Record.read_typ/cert_typ; spelling;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 adapted LocalTheory.declaration;
2009-10-27 wenzelm 2009-10-27 critical comments;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-23 hoelzl 2009-09-23 Undo errornous commit of Statespace change
2009-09-23 hoelzl 2009-09-23 correct variable order in approximate-method
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-25 wenzelm 2009-07-25 Method.Basic: no position;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 minimal adaptions for abstract binding type;
2009-03-05 wenzelm 2009-03-05 removed spurious occurrences of old rep_ss;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-04 haftmann 2009-03-04 less arbitrary occurrences of undefined
2009-01-07 haftmann 2009-01-07 changed locale predicate name convention
2009-01-06 haftmann 2009-01-06 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2009-01-01 wenzelm 2009-01-01 avoid implicit use of prems;
2008-12-18 Norbert Schirmer 2008-12-18 adapted statespace module to new locales;
2008-12-10 wenzelm 2008-12-10 more antiquotations;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-17 haftmann 2008-11-17 adjusted locale signature to *_cmd convention
2008-09-29 wenzelm 2008-09-29 LocalTheory.exit_global;
2008-09-22 haftmann 2008-09-22 fixed headers
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2008-06-19 wenzelm 2008-06-19 tuned signature; removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);
2008-06-19 wenzelm 2008-06-19 tuned signature; removed duplicate of RecordPackage.read_typ; replaced Typetab by existing Typtab;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (not really needed);
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2007-12-18 wenzelm 2007-12-18 PrintMode.setmp (avoid direct access to print_mode ref);
2007-11-12 schirmer 2007-11-12 added signatures; tuned