| 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
|