| 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
|
| Fri, 28 Oct 2005 22:27:54 +0200 |
wenzelm |
added add_local/add_global;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:52 +0200 |
wenzelm |
added incr_indexes;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:51 +0200 |
wenzelm |
renamed Goal constant to prop;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:47 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:46 +0200 |
wenzelm |
Logic.unprotect;
|
changeset |
files
|