2015-03-19 wenzelm 2015-03-19 more position information;
2014-01-26 wenzelm 2014-01-26 tuned signature;
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-08-18 haftmann 2010-08-18 deglobalization
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
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-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
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 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-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in packages;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-06-18 wenzelm 2008-06-18 eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 RuleInsts.read_instantiate;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-01 wenzelm 2008-03-01 misc cleanup of embedded ML code; use more antiquotations; tuned;
2008-02-11 wenzelm 2008-02-11 removed unnecessary theory qualifiers;
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2007-06-19 wenzelm 2007-06-19 BalancedTree;
2007-05-31 wenzelm 2007-05-31 removed obsolete IFOL.thy/FOL.thy values;
2007-04-03 wenzelm 2007-04-03 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2006-11-26 wenzelm 2006-11-26 converted legacy ML scripts;
2005-11-16 wenzelm 2005-11-16 Term.betapply;
2005-10-25 wenzelm 2005-10-25 traceIt: plain term;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms and lists;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2002-05-15 paulson 2002-05-15 better error messages for datatypes not declared Const
2001-11-19 wenzelm 2001-11-19 tuned;
2000-05-05 wenzelm 2000-05-05 use Sign.simple_read_term;
1999-10-04 wenzelm 1999-10-04 tryres, gen_make_elim moved here;
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-12 wenzelm 1999-01-12 eliminated global/local names;
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1998-05-27 paulson 1998-05-27 mk_all_imp: no longer creates goals that have beta-redexes
1998-04-10 paulson 1998-04-10 Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct
1997-12-03 paulson 1997-12-03 Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
1997-10-17 wenzelm 1997-10-17 (co) inductive / datatype package adapted to qualified names;
1996-11-28 paulson 1996-11-28 Replaced map...~~ by
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-05-08 paulson 1996-05-08 moved ap_split to cartprod.ML
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-22 paulson 1995-12-22 Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule. intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of generating a new one. Inductive defs no longer export sumprod_free_SEs ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store. Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items no longer exported. mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.
1994-11-24 lcp 1994-11-24 data_domain,Codata_domain: removed replicate; now return one single domain
1994-08-25 lcp 1994-08-25 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils
1994-08-19 wenzelm 1994-08-19 replaced Lexicon.scan_id by Scanner.scan_id; replaced const_name by Syntax.const_name;
1994-08-18 lcp 1994-08-18 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML ZF/ind_syntax/prove_term: deleted ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and Logic.unvarify
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-12 clasohm 1994-07-12 removed flatten_typ and replaced add_consts by add_consts_i
1994-07-11 clasohm 1994-07-11 removed flatten_term and replaced add_axioms by add_axioms_i
1994-07-01 clasohm 1994-07-01 replaced extend_theory by new add_* functions; changed syntax of datatype declaration