| Fri, 23 Oct 2009 16:37:56 +0200 |
krauss |
renamed auto_term.ML -> relation.ML
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:22:10 +0200 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 15:33:19 +0200 |
krauss |
renamed FundefDatatype -> Function_Fun
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 14:33:07 +0200 |
krauss |
pat_completeness gets its own file
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 21:47:41 +0200 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 21:29:04 +0100 |
wenzelm |
keep dead code fresh;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:56:49 +0100 |
haftmann |
min_weak_def [code del]
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 08:45:46 +0100 |
haftmann |
explicitly delete some code equations
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:31 +0100 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 19:24:55 +0100 |
wenzelm |
proper document antiquotations;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 08:46:07 +0100 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 11:46:14 +0200 |
krauss |
generalized induct_scheme method to prove conditional induction schemes.
|
file |
diff |
annotate
|
| Mon, 12 May 2008 22:11:06 +0200 |
krauss |
Measure functions can now be declared via special rules, allowing for a
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 16:28:06 +0200 |
krauss |
* New attribute "termination_simp": Simp rules for termination proofs
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
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
|
| Thu, 06 Dec 2007 12:58:01 +0100 |
krauss |
load sum_tree.ML
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:42 +0200 |
haftmann |
re-eliminated Option.thy
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:38:44 +0200 |
haftmann |
split off theory Option for benefit of code generator
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:03:11 +0200 |
berghofe |
Inserted definition of in_rel again (since member2 was removed).
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 12:16:27 +0200 |
krauss |
removed "sum_tools.ML" in favour of BalancedTree
|
file |
diff |
annotate
|
| Sat, 02 Jun 2007 15:28:38 +0200 |
krauss |
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:48 +0200 |
haftmann |
explicit import of Datatype.thy due to hook bootstrap problem
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:49:23 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 16:39:10 +0200 |
wenzelm |
added header;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 14:11:01 +0200 |
krauss |
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
|
file |
diff |
annotate
|
| Thu, 15 Feb 2007 17:35:19 +0100 |
krauss |
changed termination goal to use object quantifier
|
file |
diff |
annotate
|