src/HOL/Statespace/state_fun.ML
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-11-28 wenzelm 2011-11-28 more antiquotations;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-06 wenzelm 2011-11-06 misc tuning and modernization; more antiquotations;
2011-11-06 wenzelm 2011-11-06 tuned;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-17 wenzelm 2010-12-17 tuned signature;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
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-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-07-27 haftmann 2010-07-27 delete structure Basic_Record; avoid `record` in names in structure Record
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-04-15 wenzelm 2010-04-15 spelling;
2010-03-28 wenzelm 2010-03-28 tuned;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-19 wenzelm 2009-10-19 eliminated duplicate fold1 -- beware of argument order!
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
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-10-13 haftmann 2009-10-13 dropped Datatype.distinct_simproc; tuned
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
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-01-01 wenzelm 2009-01-01 normalized some ML type/val aliases;
2008-12-10 wenzelm 2008-12-10 more antiquotations;
2008-09-22 haftmann 2008-09-22 fixed headers
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-09 wenzelm 2008-06-09 DatatypePackage.distinct_simproc;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2007-11-12 schirmer 2007-11-12 added signatures; tuned
2007-10-24 schirmer 2007-10-24 added Statespace library