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;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip