| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:18 +0200 |
haftmann |
tuned of_nat code generation
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 14:49:53 +0200 |
haftmann |
moved class wellorder to theory Orderings
|
file |
diff |
annotate
|
| Fri, 08 Aug 2008 09:26:15 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 17 Jul 2008 15:21:52 +0200 |
krauss |
simplified proofs
|
file |
diff |
annotate
|
| Thu, 17 Jul 2008 13:50:17 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 23:20:05 +0200 |
wenzelm |
removed obsolete nat_induct_tac -- cannot work without;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 19:15:21 +0200 |
wenzelm |
added nat_induct_tac (works without context);
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:33 +0200 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 18:15:25 +0100 |
wenzelm |
removed redundant Nat.less_not_sym, Nat.less_asym;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2008 20:33:29 +0100 |
wenzelm |
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:00 +0100 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:14 +0100 |
haftmann |
tuned heading
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 11:18:43 +0100 |
bulwahn |
Added useful general lemmas from the work with the HeapMonad
|
file |
diff |
annotate
|
| Wed, 20 Feb 2008 14:52:38 +0100 |
haftmann |
tuned structures in arith_data.ML
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Mon, 21 Jan 2008 08:43:27 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 12:26:24 +0100 |
berghofe |
Renamed *.size to prod.size.
|
file |
diff |
annotate
|
| Thu, 13 Dec 2007 07:09:00 +0100 |
haftmann |
added lemma
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Thu, 06 Dec 2007 17:05:44 +0100 |
haftmann |
temporary code generator work arounds
|
file |
diff |
annotate
|
| Thu, 06 Dec 2007 16:36:19 +0100 |
haftmann |
authentic primrec
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:45 +0100 |
haftmann |
simplified infrastructure for code generator operational equality
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:03 +0100 |
haftmann |
adjustions to due to instance target
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:37 +0100 |
haftmann |
dropped implicit assumption proof
|
file |
diff |
annotate
|