Mon, 09 Oct 2006 19:37:03 +0200 |
wenzelm |
added General/secure.ML;
|
changeset |
files
|
Mon, 09 Oct 2006 19:37:02 +0200 |
wenzelm |
added option -S (secure mode);
|
changeset |
files
|
Mon, 09 Oct 2006 12:51:31 +0200 |
nipkow |
added nbe_post for delayed_if
|
changeset |
files
|
Mon, 09 Oct 2006 12:20:39 +0200 |
nipkow |
added delayed_if
|
changeset |
files
|
Mon, 09 Oct 2006 12:16:29 +0200 |
nipkow |
added pre/post-processor equations
|
changeset |
files
|
Mon, 09 Oct 2006 12:08:33 +0200 |
wenzelm |
attribute "symmetric": standardized schematic variables;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:11 +0200 |
wenzelm |
sequential lemmas;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:10 +0200 |
wenzelm |
reorderd ML/lemmas (Why!?);
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:09 +0200 |
wenzelm |
PureThy.note_thmss_i;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:08 +0200 |
wenzelm |
added exit;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:07 +0200 |
wenzelm |
added theorems(_i) -- with present_results;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:06 +0200 |
wenzelm |
def(_i): LocalDefs.add_defs;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:05 +0200 |
wenzelm |
attribute: Context.mapping;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:04 +0200 |
wenzelm |
removed obsolete note_thmss(_i);
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:04 +0200 |
wenzelm |
added exit;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:02 +0200 |
wenzelm |
simplified derived_def;
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:01 +0200 |
wenzelm |
removed theorems, smart_theorems etc. (cf. Specification.theorems);
|
changeset |
files
|
Mon, 09 Oct 2006 02:20:01 +0200 |
wenzelm |
lemmas/theorems/declare: Specification.theorems;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:58 +0200 |
wenzelm |
added kind attributes;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:57 +0200 |
wenzelm |
Drule.lhs/rhs_of;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:56 +0200 |
wenzelm |
added dest_equals_lhs;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:55 +0200 |
wenzelm |
attribute: Context.mapping;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:54 +0200 |
wenzelm |
replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:54 +0200 |
wenzelm |
attribute: Context.mapping;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:52 +0200 |
wenzelm |
standardized facts;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:51 +0200 |
wenzelm |
attribute symmetric: zero_var_indexes;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:51 +0200 |
wenzelm |
attribute symmetric: zero_var_indexes;
|
changeset |
files
|
Mon, 09 Oct 2006 02:19:49 +0200 |
wenzelm |
attribute: Context.mapping;
|
changeset |
files
|