Wed, 08 Apr 2015 19:39:08 +0200 | wenzelm | proper context for Object_Logic operations; | file | diff | annotate |
Mon, 06 Apr 2015 23:14:05 +0200 | wenzelm | local setup of induction tools, with restricted access to auxiliary consts; | file | diff | annotate |
Mon, 06 Apr 2015 13:28:54 +0200 | wenzelm | proper header; | file | diff | annotate |
Wed, 04 Mar 2015 19:53:18 +0100 | wenzelm | tuned signature -- prefer qualified names; | file | diff | annotate |
Wed, 29 Oct 2014 19:01:49 +0100 | wenzelm | modernized setup; | file | diff | annotate |
Thu, 10 Apr 2014 10:36:29 +0200 | wenzelm | tuned; | file | diff | annotate |
Tue, 20 Sep 2011 05:47:11 +0200 | nipkow | New proof method "induction" that gives induction hypotheses the name IH. | file | diff | annotate |