Fri, 19 Mar 1999 11:26:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 19 Mar 1999 11:24:00 +0100 |
wenzelm |
common qed and end of proofs;
|
changeset |
files
|
Thu, 18 Mar 1999 16:44:53 +0100 |
nipkow |
* New bounded quantifier syntax (input only):
|
changeset |
files
|
Thu, 18 Mar 1999 16:42:34 +0100 |
nipkow |
New bounded quantifier syntax: !x<i. P etc
|
changeset |
files
|
Thu, 18 Mar 1999 11:19:03 +0100 |
paulson |
added new theory Yahalom_Bad
|
changeset |
files
|
Thu, 18 Mar 1999 10:41:33 +0100 |
paulson |
added new theory Yahalom_Bad
|
changeset |
files
|
Thu, 18 Mar 1999 10:41:00 +0100 |
paulson |
exchanged the order of Gets and Notes in datatype event
|
changeset |
files
|
Wed, 17 Mar 1999 18:01:41 +0100 |
wenzelm |
fixed thm_name again;
|
changeset |
files
|
Wed, 17 Mar 1999 17:20:36 +0100 |
wenzelm |
Theory.sign_of;
|
changeset |
files
|
Wed, 17 Mar 1999 17:19:18 +0100 |
wenzelm |
xnum token class;
|
changeset |
files
|
Wed, 17 Mar 1999 17:18:54 +0100 |
wenzelm |
xstr token class;
|
changeset |
files
|
Wed, 17 Mar 1999 16:53:46 +0100 |
wenzelm |
Theory.sign_of;
|
changeset |
files
|
Wed, 17 Mar 1999 16:53:32 +0100 |
wenzelm |
fixed axclass_tac;
|
changeset |
files
|
Wed, 17 Mar 1999 16:45:53 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 17 Mar 1999 16:33:47 +0100 |
wenzelm |
Theory.sign_of;
|
changeset |
files
|
Wed, 17 Mar 1999 16:33:00 +0100 |
wenzelm |
qualify Theory.sign_of etc.;
|
changeset |
files
|
Wed, 17 Mar 1999 16:32:38 +0100 |
wenzelm |
fixed msg;
|
changeset |
files
|
Wed, 17 Mar 1999 15:43:04 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
Wed, 17 Mar 1999 13:56:29 +0100 |
wenzelm |
axclass_tac lost an argument;
|
changeset |
files
|
Wed, 17 Mar 1999 13:54:42 +0100 |
wenzelm |
HOL/typedef: fixed type inference for representing set;
|
changeset |
files
|
Wed, 17 Mar 1999 13:50:51 +0100 |
wenzelm |
rep_datatype: '_i' version, attributes, outer syntax;
|
changeset |
files
|
Wed, 17 Mar 1999 13:49:39 +0100 |
wenzelm |
local open OuterParse;
|
changeset |
files
|
Wed, 17 Mar 1999 13:49:14 +0100 |
wenzelm |
actually check non-emptiness theorem;
|
changeset |
files
|
Wed, 17 Mar 1999 13:47:34 +0100 |
wenzelm |
fixed typedef representing set;
|
changeset |
files
|
Wed, 17 Mar 1999 13:47:04 +0100 |
wenzelm |
adapted rep_datatype;
|
changeset |
files
|
Wed, 17 Mar 1999 13:46:23 +0100 |
wenzelm |
added dest_mem;
|
changeset |
files
|
Wed, 17 Mar 1999 13:44:43 +0100 |
wenzelm |
theory data;
|
changeset |
files
|
Wed, 17 Mar 1999 13:42:42 +0100 |
wenzelm |
adapted AxClass.add_axclass;
|
changeset |
files
|
Wed, 17 Mar 1999 13:41:50 +0100 |
wenzelm |
tuned msgs;
|
changeset |
files
|
Wed, 17 Mar 1999 13:41:14 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 17 Mar 1999 13:40:21 +0100 |
wenzelm |
cleaned comments;
|
changeset |
files
|
Wed, 17 Mar 1999 13:39:44 +0100 |
wenzelm |
added apply_cond_open;
|
changeset |
files
|
Wed, 17 Mar 1999 13:39:21 +0100 |
wenzelm |
added (improper_)command;
|
changeset |
files
|
Wed, 17 Mar 1999 13:39:01 +0100 |
wenzelm |
added simple_arity, spec_name, spec_opt_name;
|
changeset |
files
|
Wed, 17 Mar 1999 13:36:23 +0100 |
wenzelm |
added '_i' versions;
|
changeset |
files
|
Wed, 17 Mar 1999 13:34:49 +0100 |
wenzelm |
OuterSyntax.(improper_)command;
|
changeset |
files
|
Wed, 17 Mar 1999 13:33:13 +0100 |
wenzelm |
added assert_super;
|
changeset |
files
|
Wed, 17 Mar 1999 13:32:20 +0100 |
wenzelm |
added def_name;
|
changeset |
files
|
Wed, 17 Mar 1999 13:31:19 +0100 |
wenzelm |
added cond_extern_thm_sg;
|
changeset |
files
|
Wed, 17 Mar 1999 13:30:24 +0100 |
wenzelm |
AxClass.setup;
|
changeset |
files
|
Wed, 17 Mar 1999 13:30:09 +0100 |
wenzelm |
axclass.ML loaded after Isar;
|
changeset |
files
|
Fri, 12 Mar 1999 22:02:51 +0100 |
wenzelm |
made weblint happy;
|
changeset |
files
|
Fri, 12 Mar 1999 18:49:02 +0100 |
wenzelm |
comment;
|
changeset |
files
|
Fri, 12 Mar 1999 18:48:51 +0100 |
wenzelm |
removed obsolete user data stuff;
|
changeset |
files
|
Fri, 12 Mar 1999 18:48:11 +0100 |
wenzelm |
theory: include parent links;
|
changeset |
files
|
Thu, 11 Mar 1999 21:59:26 +0100 |
wenzelm |
outer syntax for 'datatype';
|
changeset |
files
|
Thu, 11 Mar 1999 21:58:54 +0100 |
wenzelm |
add_primrec(_i): attributes;
|
changeset |
files
|
Thu, 11 Mar 1999 21:58:12 +0100 |
wenzelm |
outer syntax for 'record';
|
changeset |
files
|
Thu, 11 Mar 1999 21:57:34 +0100 |
wenzelm |
named witnesses: PureThy.get_thmss;
|
changeset |
files
|
Thu, 11 Mar 1999 21:56:22 +0100 |
wenzelm |
primrec: empty attributes;
|
changeset |
files
|
Thu, 11 Mar 1999 21:55:23 +0100 |
wenzelm |
tuned opt_mixfix failure;
|
changeset |
files
|
Thu, 11 Mar 1999 21:53:50 +0100 |
wenzelm |
add_title;
|
changeset |
files
|
Thu, 11 Mar 1999 21:53:36 +0100 |
wenzelm |
added 'title';
|
changeset |
files
|
Thu, 11 Mar 1999 21:52:49 +0100 |
wenzelm |
tuned space;
|
changeset |
files
|
Thu, 11 Mar 1999 21:52:32 +0100 |
wenzelm |
comment;
|
changeset |
files
|
Thu, 11 Mar 1999 21:51:49 +0100 |
wenzelm |
workaround default_name problem;
|
changeset |
files
|
Thu, 11 Mar 1999 13:20:35 +0100 |
wenzelm |
removed foo_build_completed -- now handled by session management (via usedir);
|
changeset |
files
|
Thu, 11 Mar 1999 12:34:10 +0100 |
wenzelm |
include 'README';
|
changeset |
files
|
Thu, 11 Mar 1999 12:33:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 11 Mar 1999 12:32:40 +0100 |
wenzelm |
moved Thy/session.ML to Isar/session.ML;
|
changeset |
files
|