| Mon, 10 Dec 2007 11:24:03 +0100 |
haftmann |
swtiched ATP_Linkup and PreList in theory hierarchy
|
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
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 22:49:28 +0100 |
kleing |
rev_nth
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 18:18:39 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 08:31:12 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sun, 28 Oct 2007 13:18:00 +0100 |
wenzelm |
append/member: more light-weight way to declare authentic syntax;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2007 15:53:23 +0200 |
krauss |
use "fun" for definition of "member" -> authentic syntax
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 13:10:19 +0200 |
paulson |
random tidying of proofs
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:45 +0200 |
wenzelm |
avoid very slow metis invocation;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 16:09:36 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 17 Oct 2007 18:09:38 +0200 |
nipkow |
added sorted_list_of_set
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 16:28:29 +0200 |
berghofe |
list_codegen and char_codegen now call invoke_tycodegen to ensure
|
file |
diff |
annotate
|
| Mon, 01 Oct 2007 19:21:32 +0200 |
haftmann |
added some lemmas
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:59:24 +0200 |
ballarin |
Simplified proof due to improved integration of order_tac and simp.
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 10:27:43 +0200 |
nipkow |
hide successor
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 22:00:18 +0200 |
nipkow |
fixed haftmann bug
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 16:37:29 +0200 |
haftmann |
fixed wrong syntax treatment in class target
|
file |
diff |
annotate
|
| Wed, 19 Sep 2007 17:16:40 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 19 Sep 2007 13:59:13 +0200 |
paulson |
metis too slow
|
file |
diff |
annotate
|
| Wed, 19 Sep 2007 13:14:00 +0200 |
nipkow |
Generalized [_.._] from nat to linear orders
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:52:17 +0200 |
ballarin |
Simplified proofs due to transitivity reasoner setup.
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 17:53:37 +0200 |
paulson |
metis now available in PreList
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:22:42 +0200 |
nipkow |
sorting
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 06:21:40 +0200 |
nipkow |
sorting
|
file |
diff |
annotate
|
| Mon, 10 Sep 2007 19:21:03 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 04 Sep 2007 15:30:31 +0200 |
nipkow |
tuned lemma; replaced !! by arbitrary
|
file |
diff |
annotate
|
| Wed, 29 Aug 2007 17:25:04 +0200 |
nipkow |
turned list comprehension translations into ML to optimize base case
|
file |
diff |
annotate
|
| Wed, 29 Aug 2007 11:10:59 +0200 |
chaieb |
removed unused theorems ; added lifting properties for foldr and foldl
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:23:59 +0200 |
berghofe |
Changed "code" attribute of concat_map_singleton to "code unfold".
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 15:34:15 +0200 |
nipkow |
added (code) lemmas for setsum and foldl
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:10:13 +0200 |
nipkow |
Final mods for list comprehension
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 11:18:07 +0200 |
nipkow |
removed allpairs - use list comprehension!
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 19:24:37 +0200 |
nipkow |
removed set_concat_map and improved set_concat
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:40:34 +0200 |
haftmann |
new nbe implementation
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 17:31:10 +0200 |
berghofe |
Repaired term_of_char.
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:51 +0200 |
wenzelm |
proper simproc_setup for "list_neq";
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 18:10:28 +0200 |
nipkow |
Added lemmas
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 21:51:18 +0200 |
krauss |
renamed lemma "set_take_whileD" to "set_takeWhileD"
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:04:39 +0200 |
berghofe |
Adapted to new package for inductive sets.
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 22:27:08 +0200 |
wenzelm |
proper use of function_package ML files;
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 15:17:54 +0200 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:29 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 19:12:07 +0200 |
nipkow |
tuned list comprehension, changed filter syntax from : to <-
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 12:12:25 +0200 |
chaieb |
added a function partition and a few lemmas
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 11:00:04 +0200 |
chaieb |
added a few theorems about foldl and set
|
file |
diff |
annotate
|
| Mon, 04 Jun 2007 22:27:18 +0200 |
nipkow |
tuned list comprehension
|
file |
diff |
annotate
|
| Mon, 04 Jun 2007 15:43:31 +0200 |
haftmann |
authentic syntax for List.append
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:42 +0200 |
wenzelm |
renamed gen_submultiset to submultiset;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 16:57:51 +0200 |
nipkow |
tuned list comprehension, added lemma
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 12:58:28 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|