| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:07 +0100 |
haftmann |
added length_unique operation for code generation
|
file |
diff |
annotate
|
| Wed, 29 Oct 2008 11:33:40 +0100 |
haftmann |
explicit check for pattern discipline before code translation
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:45 +0200 |
haftmann |
code identifier namings are no longer imperative
|
file |
diff |
annotate
|
| Mon, 20 Oct 2008 23:52:59 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Thu, 09 Oct 2008 08:47:27 +0200 |
haftmann |
established canonical argument order in SML code generators
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:20 +0200 |
haftmann |
dropped superfluous if
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 09:10:02 +0200 |
haftmann |
removed obsolete name convention "func"
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 16:13:09 +0200 |
haftmann |
a sophisticated char/nibble conversion combinator
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:27 +0200 |
haftmann |
explicit size of characters
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 20:38:17 +0200 |
haftmann |
distributed literal code generation out of central infrastructure
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 22:10:42 +0200 |
nipkow |
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 19:16:40 +0200 |
nipkow |
cleaned up code generation for {.._} and {..<_}
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 10:18:37 +0200 |
haftmann |
restructured code generation of literals
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 12:57:50 +0200 |
nipkow |
made setsum executable on int.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 13:16:54 +0200 |
nipkow |
added removeAll
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 21:21:13 +0200 |
wenzelm |
@{lemma}: 'by' keyword;
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| Fri, 23 May 2008 16:41:39 +0200 |
berghofe |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
|
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
|
| Wed, 07 May 2008 10:56:37 +0200 |
berghofe |
- Explicitely applied predicate1I in a few proofs, because it is no longer
|
file |
diff |
annotate
|
| Fri, 02 May 2008 18:01:02 +0200 |
nipkow |
Added documentation
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 16:28:06 +0200 |
krauss |
* New attribute "termination_simp": Simp rules for termination proofs
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Fri, 01 Jun 2007 22:09:16 +0200 |
nipkow |
Moved list comprehension into List
|
file |
diff |
annotate
|
| Thu, 24 May 2007 22:55:53 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 21 May 2007 19:11:39 +0200 |
haftmann |
improved code for rev
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:57 +0200 |
haftmann |
constant op @ now named append
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:17 +0200 |
haftmann |
abstract size function in hologic.ML
|
file |
diff |
annotate
|
| Fri, 11 May 2007 20:07:00 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:49:44 +0200 |
haftmann |
PreList imports RecDef
|
file |
diff |
annotate
|
| Wed, 02 May 2007 21:00:06 +0200 |
nipkow |
tuned allpairs
|
file |
diff |
annotate
|
| Mon, 30 Apr 2007 22:43:33 +0200 |
nipkow |
added allpairs
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:32:59 +0200 |
haftmann |
moved code generation pretty integers and characters to separate theories
|
file |
diff |
annotate
|
| Wed, 25 Apr 2007 17:50:48 +0200 |
nipkow |
new lemma splice_length
|
file |
diff |
annotate
|
| Wed, 11 Apr 2007 08:28:14 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 30 Mar 2007 16:19:00 +0200 |
haftmann |
paraphrasing equality
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 10:47:19 +0200 |
berghofe |
Improved code generator for characters: now handles
|
file |
diff |
annotate
|
| Fri, 23 Mar 2007 09:40:49 +0100 |
haftmann |
two further properties about lists
|
file |
diff |
annotate
|
| Wed, 21 Mar 2007 16:07:40 +0100 |
krauss |
added another rule for simultaneous induction, and lemmas for zip
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:28:09 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 13:27:41 +0100 |
nipkow |
Added simproc list_neq (prompted by an application)
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
file |
diff |
annotate
|
| Thu, 21 Dec 2006 13:55:11 +0100 |
haftmann |
added code lemmas for quantification over bounded nats
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:27 +0100 |
haftmann |
added code generation syntax for some char combinators
|
file |
diff |
annotate
|