| 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.
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 03 Nov 2005 02:37:09 +0100 |
huffman |
reimplement copy_def to use data constructor constants
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 03 Nov 2005 01:54:51 +0100 |
huffman |
generate lambda pattern syntax for new data constructors
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 03 Nov 2005 01:44:27 +0100 |
huffman |
add constant one_when; LAM pattern for ONE
|
changeset |
files
|
| Thu, 03 Nov 2005 01:28:22 +0100 |
huffman |
add translation for wildcard pattern
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 03 Nov 2005 01:02:29 +0100 |
huffman |
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
|
changeset |
files
|
| Thu, 03 Nov 2005 00:57:35 +0100 |
huffman |
cleaned up; ch2ch_Rep_CFun is a simp rule
|
changeset |
files
|
| Thu, 03 Nov 2005 00:43:50 +0100 |
huffman |
changed iterate to a continuous type
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 03 Nov 2005 00:32:47 +0100 |
huffman |
removed ex/loeckx.ML
|
changeset |
files
|
| Thu, 03 Nov 2005 00:31:32 +0100 |
huffman |
removed proof about Ifix, which no longer exists
|
changeset |
files
|
| Thu, 03 Nov 2005 00:16:09 +0100 |
huffman |
cleaned up; chain_const and thelub_const are simp rules
|
changeset |
files
|
| Thu, 03 Nov 2005 00:12:29 +0100 |
huffman |
cleaned up; removed adm_tricks in favor of compactness theorems
|
changeset |
files
|
| Wed, 02 Nov 2005 23:59:49 +0100 |
huffman |
fix spelling
|
changeset |
files
|
| Wed, 02 Nov 2005 16:37:39 +0100 |
berghofe |
Moved atom stuff to new file nominal_atoms.ML
|
changeset |
files
|
| Wed, 02 Nov 2005 15:31:12 +0100 |
urbanc |
- completed the list of thms for supp_atm
|
changeset |
files
|
| Wed, 02 Nov 2005 15:05:22 +0100 |
berghofe |
Added code for proving that new datatype has finite support.
|
changeset |
files
|
| Wed, 02 Nov 2005 14:48:55 +0100 |
wenzelm |
removed unused modify_typargs, map_typargs, fold_typargs;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:47:01 +0100 |
wenzelm |
added Isar.state/exn;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:47:00 +0100 |
wenzelm |
Isar.loop;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:58 +0100 |
wenzelm |
moved consts declarations to consts.ML;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:57 +0100 |
wenzelm |
Consts.dest;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:56 +0100 |
wenzelm |
Polymorphic constants.
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:54 +0100 |
wenzelm |
added consts.ML;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:53 +0100 |
wenzelm |
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:51 +0100 |
wenzelm |
dist_eqI: the_context();
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:49 +0100 |
wenzelm |
Sign.const_monomorphic;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:47 +0100 |
wenzelm |
Logic.nth_prem;
|
changeset |
files
|
| Wed, 02 Nov 2005 11:02:29 +0100 |
urbanc |
added the collection of lemmas "supp_at"
|
changeset |
files
|
| Tue, 01 Nov 2005 23:55:53 +0100 |
urbanc |
some minor tweaks in some proofs (nothing extraordinary)
|
changeset |
files
|
| Tue, 01 Nov 2005 23:54:29 +0100 |
urbanc |
tunings of some comments (nothing serious)
|
changeset |
files
|
| Mon, 31 Oct 2005 16:35:15 +0100 |
haftmann |
nth_*, fold_index refined
|
changeset |
files
|
| Mon, 31 Oct 2005 16:00:15 +0100 |
haftmann |
fold_index replacing foldln
|
changeset |
files
|
| Mon, 31 Oct 2005 01:43:22 +0100 |
nipkow |
A few new lemmas
|
changeset |
files
|
| Sun, 30 Oct 2005 10:55:56 +0100 |
urbanc |
tuned my last commit
|
changeset |
files
|
| Sun, 30 Oct 2005 10:37:57 +0100 |
urbanc |
simplified the abs_supp_approx proof and tuned some comments in
|
changeset |
files
|
| Sat, 29 Oct 2005 15:01:25 +0200 |
urbanc |
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
|
changeset |
files
|
| Sat, 29 Oct 2005 14:37:32 +0200 |
urbanc |
1) have adjusted the swapping of the result type
|
changeset |
files
|
| Fri, 28 Oct 2005 22:37:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:32:55 +0200 |
wenzelm |
lthms_containing: not o valid_thms;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:15 +0200 |
wenzelm |
added fact_tac, some_fact_tac;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:13 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:12 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:11 +0200 |
wenzelm |
added fact method;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:09 +0200 |
wenzelm |
tuned ProofContext.export interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:07 +0200 |
wenzelm |
syntax for literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:06 +0200 |
wenzelm |
removed try_dest_Goal, use Logic.unprotect;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:04 +0200 |
wenzelm |
added cgoal_of;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:03 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:02 +0200 |
wenzelm |
export cong_modifiers, simp_modifiers';
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:00 +0200 |
wenzelm |
certify_term: tuned monomorphic consts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:59 +0200 |
wenzelm |
datatype thmref: added Fact;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:58 +0200 |
wenzelm |
Logic.lift_all;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:57 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:56 +0200 |
wenzelm |
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:55 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|