Thu, 11 Jul 2002 10:48:30 +0200 *** empty log message ***
nipkow [Thu, 11 Jul 2002 10:48:30 +0200] rev 13347
*** empty log message ***
Thu, 11 Jul 2002 09:47:15 +0200 Added partly automated version of Newman.
nipkow [Thu, 11 Jul 2002 09:47:15 +0200] rev 13346
Added partly automated version of Newman.
Thu, 11 Jul 2002 09:36:41 +0200 Fixed markup error in comment.
schirmer [Thu, 11 Jul 2002 09:36:41 +0200] rev 13345
Fixed markup error in comment.
Thu, 11 Jul 2002 09:31:01 +0200 *** empty log message ***
nipkow [Thu, 11 Jul 2002 09:31:01 +0200] rev 13344
*** empty log message ***
Thu, 11 Jul 2002 09:17:01 +0200 *** empty log message ***
nipkow [Thu, 11 Jul 2002 09:17:01 +0200] rev 13343
*** empty log message ***
Wed, 10 Jul 2002 18:39:15 +0200 expand_proof now also takes an optional term describing the proposition
berghofe [Wed, 10 Jul 2002 18:39:15 +0200] rev 13342
expand_proof now also takes an optional term describing the proposition of the theorem to be expanded (to avoid problems with different theorems having the same names).
Wed, 10 Jul 2002 18:37:51 +0200 - Moved abs_def to drule.ML
berghofe [Wed, 10 Jul 2002 18:37:51 +0200] rev 13341
- Moved abs_def to drule.ML - elim_defs now takes a boolean argument which controls the automatic expansion of theorems mentioning constants whose definitions are eliminated
Wed, 10 Jul 2002 18:35:34 +0200 Simplified proof of induction rule for datatypes involving function types.
berghofe [Wed, 10 Jul 2002 18:35:34 +0200] rev 13340
Simplified proof of induction rule for datatypes involving function types.
Wed, 10 Jul 2002 16:54:07 +0200 Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson [Wed, 10 Jul 2002 16:54:07 +0200] rev 13339
Fixed quantified variable name preservation for ball and bex (bounded quants) Requires tweaking of other scripts. Also routine tidying.
Wed, 10 Jul 2002 16:07:52 +0200 *** empty log message ***
nipkow [Wed, 10 Jul 2002 16:07:52 +0200] rev 13338
*** empty log message ***
Wed, 10 Jul 2002 15:07:02 +0200 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer [Wed, 10 Jul 2002 15:07:02 +0200] rev 13337
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
Wed, 10 Jul 2002 14:51:18 +0200 tuned add_thmss;
wenzelm [Wed, 10 Jul 2002 14:51:18 +0200] rev 13336
tuned add_thmss; beginnings of locale predicates;
Wed, 10 Jul 2002 14:50:08 +0200 tuned Locale.add_thmss;
wenzelm [Wed, 10 Jul 2002 14:50:08 +0200] rev 13335
tuned Locale.add_thmss;
Wed, 10 Jul 2002 14:49:06 +0200 added assert_judgment;
wenzelm [Wed, 10 Jul 2002 14:49:06 +0200] rev 13334
added assert_judgment;
Wed, 10 Jul 2002 14:48:08 +0200 NameSpace.accesses';
wenzelm [Wed, 10 Jul 2002 14:48:08 +0200] rev 13333
NameSpace.accesses';
Wed, 10 Jul 2002 14:47:48 +0200 added accesses';
wenzelm [Wed, 10 Jul 2002 14:47:48 +0200] rev 13332
added accesses';
Wed, 10 Jul 2002 13:55:32 +0200 tuned;
wenzelm [Wed, 10 Jul 2002 13:55:32 +0200] rev 13331
tuned;
Wed, 10 Jul 2002 08:09:35 +0200 *** empty log message ***
nipkow [Wed, 10 Jul 2002 08:09:35 +0200] rev 13330
*** empty log message ***
Wed, 10 Jul 2002 07:20:02 +0200 *** empty log message ***
nipkow [Wed, 10 Jul 2002 07:20:02 +0200] rev 13329
*** empty log message ***
Tue, 09 Jul 2002 23:05:26 +0200 better document preparation
paulson [Tue, 09 Jul 2002 23:05:26 +0200] rev 13328
better document preparation
Tue, 09 Jul 2002 23:03:21 +0200 converted List to new-style
paulson [Tue, 09 Jul 2002 23:03:21 +0200] rev 13327
converted List to new-style
Tue, 09 Jul 2002 18:54:27 +0200 *** empty log message ***
nipkow [Tue, 09 Jul 2002 18:54:27 +0200] rev 13326
*** empty log message ***
Tue, 09 Jul 2002 18:03:26 +0200 Added function abs_def.
berghofe [Tue, 09 Jul 2002 18:03:26 +0200] rev 13325
Added function abs_def.
Tue, 09 Jul 2002 17:25:42 +0200 more and simpler separation proofs
paulson [Tue, 09 Jul 2002 17:25:42 +0200] rev 13324
more and simpler separation proofs
Tue, 09 Jul 2002 15:39:44 +0200 More relativization, reflection and proofs of separation
paulson [Tue, 09 Jul 2002 15:39:44 +0200] rev 13323
More relativization, reflection and proofs of separation
Tue, 09 Jul 2002 13:41:38 +0200 *** empty log message ***
nipkow [Tue, 09 Jul 2002 13:41:38 +0200] rev 13322
*** empty log message ***
Tue, 09 Jul 2002 11:55:46 +0200 tuned;
wenzelm [Tue, 09 Jul 2002 11:55:46 +0200] rev 13321
tuned;
Tue, 09 Jul 2002 11:46:36 +0200 send email plaform independently
isatest [Tue, 09 Jul 2002 11:46:36 +0200] rev 13320
send email plaform independently
Tue, 09 Jul 2002 10:44:53 +0200 More Separation proofs
paulson [Tue, 09 Jul 2002 10:44:53 +0200] rev 13319
More Separation proofs
Tue, 09 Jul 2002 10:44:41 +0200 new files
paulson [Tue, 09 Jul 2002 10:44:41 +0200] rev 13318
new files
(0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip