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