Fri, 28 Oct 2005 22:27:51 +0200 renamed Goal constant to prop;
wenzelm [Fri, 28 Oct 2005 22:27:51 +0200] rev 18024
renamed Goal constant to prop;
Fri, 28 Oct 2005 22:27:47 +0200 accomodate simplified Thm.lift_rule;
wenzelm [Fri, 28 Oct 2005 22:27:47 +0200] rev 18023
accomodate simplified Thm.lift_rule;
Fri, 28 Oct 2005 22:27:46 +0200 Logic.unprotect;
wenzelm [Fri, 28 Oct 2005 22:27:46 +0200] rev 18022
Logic.unprotect;
Fri, 28 Oct 2005 22:27:44 +0200 literal facts;
wenzelm [Fri, 28 Oct 2005 22:27:44 +0200] rev 18021
literal facts;
Fri, 28 Oct 2005 22:27:41 +0200 * Pure/Isar: literal facts;
wenzelm [Fri, 28 Oct 2005 22:27:41 +0200] rev 18020
* Pure/Isar: literal facts; * ML/Pure: tuned Thm.lift_rule; * ML/Pure: renamed Goal constant to prop, more general uses;
Fri, 28 Oct 2005 22:26:10 +0200 tuned;
wenzelm [Fri, 28 Oct 2005 22:26:10 +0200] rev 18019
tuned;
Fri, 28 Oct 2005 20:18:37 +0200 unnecessary imports removed
webertj [Fri, 28 Oct 2005 20:18:37 +0200] rev 18018
unnecessary imports removed
Fri, 28 Oct 2005 18:53:26 +0200 fixed case names in the weak induction principle and
urbanc [Fri, 28 Oct 2005 18:53:26 +0200] rev 18017
fixed case names in the weak induction principle and changed name from "induct" to "induct_weak"
Fri, 28 Oct 2005 18:22:26 +0200 Implemented proof of weak induction theorem.
berghofe [Fri, 28 Oct 2005 18:22:26 +0200] rev 18016
Implemented proof of weak induction theorem.
Fri, 28 Oct 2005 17:59:07 +0200 Added "deepen" method.
berghofe [Fri, 28 Oct 2005 17:59:07 +0200] rev 18015
Added "deepen" method.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip