src/ZF/ind_syntax.ML
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
1993-09-17 lcp 1993-09-17 Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.