Wed, 02 Jul 1997 11:59:10 +0200 | nipkow | Added the following lemmas tp Divides and a few others to Arith and NatDef: | file | diff | annotate |
Mon, 23 Jun 1997 10:42:03 +0200 | paulson | Ran expandshort | file | diff | annotate |
Wed, 18 Jun 1997 15:31:31 +0200 | paulson | Addition of not_imp (which pushes negation into implication) as a default | file | diff | annotate |
Fri, 13 Jun 1997 10:35:13 +0200 | nipkow | Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas. | file | diff | annotate |
Thu, 05 Jun 1997 14:39:22 +0200 | nipkow | Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. | file | diff | annotate |
Thu, 22 May 1997 15:09:37 +0200 | paulson | Deleted rprod: lex_prod is (usually?) enough | file | diff | annotate |
Tue, 20 May 1997 11:40:28 +0200 | paulson | Relation "less_than" internalizes "<" for easy use of TFL | file | diff | annotate |
Thu, 15 May 1997 12:45:42 +0200 | paulson | New theories used by TFL | file | diff | annotate |