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
2005-11-03 huffman 2005-11-03 cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
2005-11-03 huffman 2005-11-03 generate lambda pattern syntax for new data constructors
2005-11-03 huffman 2005-11-03 changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
2005-11-03 huffman 2005-11-03 add constant one_when; LAM pattern for ONE
2005-11-03 huffman 2005-11-03 add translation for wildcard pattern
2005-11-03 huffman 2005-11-03 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
2005-11-03 huffman 2005-11-03 make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
2005-11-03 huffman 2005-11-03 cleaned up; ch2ch_Rep_CFun is a simp rule
2005-11-03 huffman 2005-11-03 changed iterate to a continuous type
2005-11-03 huffman 2005-11-03 reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
2005-11-03 huffman 2005-11-03 removed ex/loeckx.ML
2005-11-03 huffman 2005-11-03 removed proof about Ifix, which no longer exists
2005-11-03 huffman 2005-11-03 cleaned up; chain_const and thelub_const are simp rules
2005-11-03 huffman 2005-11-03 cleaned up; removed adm_tricks in favor of compactness theorems
2005-11-02 huffman 2005-11-02 fix spelling
2005-11-02 berghofe 2005-11-02 Moved atom stuff to new file nominal_atoms.ML
2005-11-02 urbanc 2005-11-02 - completed the list of thms for supp_atm - cleaned up the way how thms are collected under single names
2005-11-02 berghofe 2005-11-02 Added code for proving that new datatype has finite support.
2005-11-02 wenzelm 2005-11-02 removed unused modify_typargs, map_typargs, fold_typargs;
2005-11-02 wenzelm 2005-11-02 added Isar.state/exn;
2005-11-02 wenzelm 2005-11-02 Isar.loop;
2005-11-02 wenzelm 2005-11-02 moved consts declarations to consts.ML;
2005-11-02 wenzelm 2005-11-02 Consts.dest;
2005-11-02 wenzelm 2005-11-02 Polymorphic constants.
2005-11-02 wenzelm 2005-11-02 added consts.ML;
2005-11-02 wenzelm 2005-11-02 fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
2005-11-02 wenzelm 2005-11-02 dist_eqI: the_context();
2005-11-02 wenzelm 2005-11-02 Sign.const_monomorphic;
2005-11-02 wenzelm 2005-11-02 Logic.nth_prem;
2005-11-02 urbanc 2005-11-02 added the collection of lemmas "supp_at"
2005-11-01 urbanc 2005-11-01 some minor tweaks in some proofs (nothing extraordinary)
2005-11-01 urbanc 2005-11-01 tunings of some comments (nothing serious)
2005-10-31 haftmann 2005-10-31 nth_*, fold_index refined
2005-10-31 haftmann 2005-10-31 fold_index replacing foldln
2005-10-31 nipkow 2005-10-31 A few new lemmas
2005-10-30 urbanc 2005-10-30 tuned my last commit
2005-10-30 urbanc 2005-10-30 simplified the abs_supp_approx proof and tuned some comments in nominal_permeq.ML
2005-10-29 urbanc 2005-10-29 Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'. This means the syntax of the tactics supports_simp and perm_simp are exactly like simp, namely (supports_simp add: .... del: ...) where the add's and del's are optional.
2005-10-29 urbanc 2005-10-29 1) have adjusted the swapping of the result type in add_datatype_i 2) have replaced map_nth_elem by Library.nth_map (there seems to be a clash with an existing nth_map somewhere - therefore the "Library")
2005-10-28 wenzelm 2005-10-28 tuned;
2005-10-28 wenzelm 2005-10-28 lthms_containing: not o valid_thms;
2005-10-28 wenzelm 2005-10-28 added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces; tuned ProofContext.export interfaces;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28 wenzelm 2005-10-28 added fact method; accomodate simplified Thm.lift_rule;
2005-10-28 wenzelm 2005-10-28 tuned ProofContext.export interfaces;