| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 15:50:06 +0100 |
wenzelm |
provide regular ML interfaces for Isar source language elements;
|
file |
diff |
annotate
|
| Sat, 27 Dec 2008 17:49:15 +0100 |
krauss |
removed duplicate sum_case used only by function package;
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 11:58:27 +0200 |
krauss |
fix: need to beta/eta normalize
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 11:46:14 +0200 |
krauss |
generalized induct_scheme method to prove conditional induction schemes.
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 16:42:47 +0200 |
krauss |
proper context for induct_scheme method
|
file |
diff |
annotate
|
| Sun, 09 Dec 2007 20:59:53 +0100 |
krauss |
added Id, some cleanup
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 09:42:20 +0100 |
krauss |
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
|
file |
diff |
annotate
|