Fri, 04 Nov 2005 22:27:40 +0100 huffman cleaned up
Fri, 04 Nov 2005 22:26:09 +0100 huffman add print translation: Abs_CFun f => LAM x. f x
Thu, 03 Nov 2005 04:31:12 +0100 mengj Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
Thu, 03 Nov 2005 03:06:02 +0100 huffman improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
Thu, 03 Nov 2005 02:37:09 +0100 huffman reimplement copy_def to use data constructor constants
Thu, 03 Nov 2005 02:19:48 +0100 huffman cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
Thu, 03 Nov 2005 01:54:51 +0100 huffman generate lambda pattern syntax for new data constructors
Thu, 03 Nov 2005 01:45:52 +0100 huffman changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
Thu, 03 Nov 2005 01:44:27 +0100 huffman add constant one_when; LAM pattern for ONE
Thu, 03 Nov 2005 01:28:22 +0100 huffman add translation for wildcard pattern
Thu, 03 Nov 2005 01:11:39 +0100 huffman change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
Thu, 03 Nov 2005 01:02:29 +0100 huffman make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
Thu, 03 Nov 2005 00:57:35 +0100 huffman cleaned up; ch2ch_Rep_CFun is a simp rule
Thu, 03 Nov 2005 00:43:50 +0100 huffman changed iterate to a continuous type
Thu, 03 Nov 2005 00:43:11 +0100 huffman reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
Thu, 03 Nov 2005 00:32:47 +0100 huffman removed ex/loeckx.ML
Thu, 03 Nov 2005 00:31:32 +0100 huffman removed proof about Ifix, which no longer exists
Thu, 03 Nov 2005 00:16:09 +0100 huffman cleaned up; chain_const and thelub_const are simp rules
Thu, 03 Nov 2005 00:12:29 +0100 huffman cleaned up; removed adm_tricks in favor of compactness theorems
Wed, 02 Nov 2005 23:59:49 +0100 huffman fix spelling
Wed, 02 Nov 2005 16:37:39 +0100 berghofe Moved atom stuff to new file nominal_atoms.ML
Wed, 02 Nov 2005 15:31:12 +0100 urbanc - completed the list of thms for supp_atm
Wed, 02 Nov 2005 15:05:22 +0100 berghofe Added code for proving that new datatype has finite support.
Wed, 02 Nov 2005 14:48:55 +0100 wenzelm removed unused modify_typargs, map_typargs, fold_typargs;
Wed, 02 Nov 2005 14:47:01 +0100 wenzelm added Isar.state/exn;
Wed, 02 Nov 2005 14:47:00 +0100 wenzelm Isar.loop;
Wed, 02 Nov 2005 14:46:58 +0100 wenzelm moved consts declarations to consts.ML;
Wed, 02 Nov 2005 14:46:57 +0100 wenzelm Consts.dest;
Wed, 02 Nov 2005 14:46:56 +0100 wenzelm Polymorphic constants.
Wed, 02 Nov 2005 14:46:54 +0100 wenzelm added consts.ML;
Wed, 02 Nov 2005 14:46:53 +0100 wenzelm fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
Wed, 02 Nov 2005 14:46:51 +0100 wenzelm dist_eqI: the_context();
Wed, 02 Nov 2005 14:46:49 +0100 wenzelm Sign.const_monomorphic;
Wed, 02 Nov 2005 14:46:47 +0100 wenzelm Logic.nth_prem;
Wed, 02 Nov 2005 11:02:29 +0100 urbanc added the collection of lemmas "supp_at"
Tue, 01 Nov 2005 23:55:53 +0100 urbanc some minor tweaks in some proofs (nothing extraordinary)
Tue, 01 Nov 2005 23:54:29 +0100 urbanc tunings of some comments (nothing serious)
Mon, 31 Oct 2005 16:35:15 +0100 haftmann nth_*, fold_index refined
Mon, 31 Oct 2005 16:00:15 +0100 haftmann fold_index replacing foldln
Mon, 31 Oct 2005 01:43:22 +0100 nipkow A few new lemmas
Sun, 30 Oct 2005 10:55:56 +0100 urbanc tuned my last commit
Sun, 30 Oct 2005 10:37:57 +0100 urbanc simplified the abs_supp_approx proof and tuned some comments in
Sat, 29 Oct 2005 15:01:25 +0200 urbanc Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
Sat, 29 Oct 2005 14:37:32 +0200 urbanc 1) have adjusted the swapping of the result type
Fri, 28 Oct 2005 22:37:57 +0200 wenzelm tuned;
Fri, 28 Oct 2005 22:32:55 +0200 wenzelm lthms_containing: not o valid_thms;
Fri, 28 Oct 2005 22:28:15 +0200 wenzelm added fact_tac, some_fact_tac;
Fri, 28 Oct 2005 22:28:13 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:28:12 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:28:11 +0200 wenzelm added fact method;
Fri, 28 Oct 2005 22:28:09 +0200 wenzelm tuned ProofContext.export interfaces;
Fri, 28 Oct 2005 22:28:07 +0200 wenzelm syntax for literal facts;
Fri, 28 Oct 2005 22:28:06 +0200 wenzelm removed try_dest_Goal, use Logic.unprotect;
Fri, 28 Oct 2005 22:28:04 +0200 wenzelm added cgoal_of;
Fri, 28 Oct 2005 22:28:03 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 28 Oct 2005 22:28:02 +0200 wenzelm export cong_modifiers, simp_modifiers';
Fri, 28 Oct 2005 22:28:00 +0200 wenzelm certify_term: tuned monomorphic consts;
Fri, 28 Oct 2005 22:27:59 +0200 wenzelm datatype thmref: added Fact;
Fri, 28 Oct 2005 22:27:58 +0200 wenzelm Logic.lift_all;
Fri, 28 Oct 2005 22:27:57 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip