2005-11-10 paulson 2005-11-10 tidying
2005-11-10 urbanc 2005-11-10 called the induction principle "unsafe" instead of "test".
2005-11-09 paulson 2005-11-09 Skolemization by inference, but not quite finished
2005-11-09 wenzelm 2005-11-09 Explicit data structures for some Isar language elements.
2005-11-09 wenzelm 2005-11-09 tuned;
2005-11-09 wenzelm 2005-11-09 tvars_intr_list: natural argument order;
2005-11-09 wenzelm 2005-11-09 moved datatype elem to element.ML; removed unused imports function;
2005-11-09 wenzelm 2005-11-09 P.context_element, P.locale_element;
2005-11-09 wenzelm 2005-11-09 Element.context;
2005-11-09 wenzelm 2005-11-09 use existing exeption Empty;
2005-11-09 wenzelm 2005-11-09 avoid code redundancy; tuned comments;
2005-11-09 wenzelm 2005-11-09 tuned comments;
2005-11-09 wenzelm 2005-11-09 removed obsolete term set operations;
2005-11-09 wenzelm 2005-11-09 P.locale_element;
2005-11-09 wenzelm 2005-11-09 added fold_terms; added tfrees_of, frees_of; tvars_intr_list: natural argument order;
2005-11-09 wenzelm 2005-11-09 added Isar/element.ML;
2005-11-09 wenzelm 2005-11-09 Thm.varifyT': natural argument order;
2005-11-09 haftmann 2005-11-09 added join function
2005-11-08 haftmann 2005-11-08 allowing indentation of 'theory' keyword
2005-11-08 wenzelm 2005-11-08 simplified after_qed;
2005-11-08 wenzelm 2005-11-08 avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;
2005-11-08 wenzelm 2005-11-08 removed export_plain; (some_)fact_tac: Drule.incr_indexes;
2005-11-08 wenzelm 2005-11-08 renamed assert_prop to ensure_prop;
2005-11-08 wenzelm 2005-11-08 renamed goals.ML to old_goals.ML; inline Drule.impose_hyps;
2005-11-08 wenzelm 2005-11-08 export compose_hhf; removed obsolete norm_hhf_plain; tuned;
2005-11-08 wenzelm 2005-11-08 removed impose_hyps, satisfy_hyps; tuned;
2005-11-08 wenzelm 2005-11-08 const args: do not store variable names (unused);
2005-11-08 wenzelm 2005-11-08 renamed goals.ML to old_goals.ML;
2005-11-08 haftmann 2005-11-08 (fix for accidental commit)
2005-11-08 haftmann 2005-11-08 (codegen)
2005-11-08 huffman 2005-11-08 generate pattern combinators for new datatypes
2005-11-07 huffman 2005-11-07 reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
2005-11-07 huffman 2005-11-07 add case syntax for type one
2005-11-07 huffman 2005-11-07 remove syntax for as-patterns
2005-11-07 wenzelm 2005-11-07 avoid 'as' as identifier;
2005-11-07 wenzelm 2005-11-07 avoid 'as' as identifier;
2005-11-07 berghofe 2005-11-07 Added strong induction theorem (currently only axiomatized!).
2005-11-07 urbanc 2005-11-07 Initial commit.
2005-11-07 urbanc 2005-11-07 Initial commit of the theory "Weakening".
2005-11-07 urbanc 2005-11-07 added thms perm, distinct and fresh to the simplifier. One would liket to add also inject, but this causes problems with "congruences" like Lam [a].t1 = Lam [b].t2 P (Lam [a].t1) ----------------------- P (Lam [b].t2) because the equation "Lam [a].t1 = Lam [b].t2" would simplify to "[a].t1 = [b].t2" and then the goal is not true just by simplification.
2005-11-07 haftmann 2005-11-07 added proper fillin_mixfix
2005-11-07 haftmann 2005-11-07 added fillin_mixfix, replace_quote
2005-11-07 berghofe 2005-11-07 New function store_thmss_atts.
2005-11-07 urbanc 2005-11-07 used the function Library.product for the cprod from Stefan
2005-11-07 urbanc 2005-11-07 fixed bug with nominal induct - the bug occured in rule inductions when the goal did not use all variables from the relation over which the induction was done
2005-11-07 haftmann 2005-11-07 added fillin_mixfix' needed by serializer
2005-11-06 huffman 2005-11-06 add case syntax stuff
2005-11-06 huffman 2005-11-06 use consts for infix syntax
2005-11-06 huffman 2005-11-06 add proof of Bekic's theorem: fix_cprod
2005-11-05 huffman 2005-11-05 simplify definitions
2005-11-05 huffman 2005-11-05 put iterate and fix in separate sections; added Letrec
2005-11-05 huffman 2005-11-05 renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-11-05 huffman 2005-11-05 add line breaks to Rep_CFun syntax
2005-11-04 huffman 2005-11-04 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
2005-11-04 huffman 2005-11-04 moved adm_chfindom from Fix.thy to Cfun.thy
2005-11-04 huffman 2005-11-04 cleaned up
2005-11-04 huffman 2005-11-04 add print translation: Abs_CFun f => LAM x. f x
2005-11-03 mengj 2005-11-03 Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names. Also removed some functions that are not used any more.
2005-11-03 huffman 2005-11-03 improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
2005-11-03 huffman 2005-11-03 reimplement copy_def to use data constructor constants