| Tue, 22 Apr 2008 08:33:20 +0200 |
haftmann |
dropped some metis calls
|
file |
diff |
annotate
|
| Wed, 09 Apr 2008 05:30:14 +0200 |
huffman |
move lemmas from Word/BinBoolList.thy to List.thy
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 19:04:36 +0100 |
haftmann |
restructuring; explicit case names for rule list_induct2
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:00 +0100 |
wenzelm |
removed duplicate lemmas;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:13 +0100 |
haftmann |
char and nibble are finite
|
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
|
| Fri, 15 Feb 2008 17:36:21 +0100 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:44 +0100 |
haftmann |
dropped superfluous code theorems
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 19:09:21 +0100 |
berghofe |
New interface for test data generators.
|
file |
diff |
annotate
|
| 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
|