src/ZF/ind_syntax.ML
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 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-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 ListPair.map
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
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying
1994-01-18 lcp 1994-01-18 Updated refs to old Sign functions
1993-12-21 nipkow 1993-12-21 added []-field to extend_theory: no type abbreviations.
1993-10-22 lcp 1993-10-22 ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works ZF/intr-elim/elim_rls: applied make_elim to succ_inject! ZF/fin: changed type_intrs in inductive def ZF/datatype/datatype_intrs, datatype_elims: renamed from data_typechecks, data_elims ZF/list: now uses datatype_intrs
1993-10-15 lcp 1993-10-15 ZF/ind-syntax/refl_thin: new ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD by dresolve_tac InlD,InrD and etac PartE
1993-09-30 lcp 1993-09-30 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed