| Mon, 17 Oct 2005 23:10:15 +0200 |
wenzelm |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:10 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 19:19:29 +0200 |
berghofe |
Improved proof of injectivity theorems to make it work on
|
changeset |
files
|
| Mon, 17 Oct 2005 18:34:51 +0200 |
berghofe |
Fixed bug in proof of support theorem (it failed on constructors with no arguments).
|
changeset |
files
|
| Mon, 17 Oct 2005 17:42:24 +0200 |
berghofe |
Implemented proofs for support and freshness theorems.
|
changeset |
files
|
| Mon, 17 Oct 2005 17:40:34 +0200 |
urbanc |
deleted leading space in the definition of fresh
|
changeset |
files
|
| Mon, 17 Oct 2005 12:30:57 +0200 |
berghofe |
Initial revision.
|
changeset |
files
|
| Sat, 15 Oct 2005 00:14:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:20 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:07 +0200 |
wenzelm |
added ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:15 +0200 |
wenzelm |
more;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:14 +0200 |
wenzelm |
* antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:13 +0200 |
wenzelm |
added guess;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:12 +0200 |
wenzelm |
added antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:11 +0200 |
wenzelm |
use perl for test/stat;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:10 +0200 |
wenzelm |
export strip_params;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:09 +0200 |
wenzelm |
note_thmss, read/cert_vars etc.: natural argument order;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:08 +0200 |
wenzelm |
goal statements: before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:07 +0200 |
wenzelm |
added 'guess', which derives the obtained context from the course of reasoning;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:06 +0200 |
wenzelm |
added primitive_text, succeed_text;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:05 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:04 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:03 +0200 |
wenzelm |
added 'guess';
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:01 +0200 |
wenzelm |
added no_facts;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:00 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:07:59 +0200 |
wenzelm |
updated;
|
changeset |
files
|