| Wed, 04 Mar 2009 11:05:29 +0100 |
Merge.
|
file | diff | annotate |
| Wed, 04 Mar 2009 10:45:52 +0100 |
Merge.
|
file | diff | annotate |
| Mon, 02 Mar 2009 16:53:55 +0100 |
name changes
|
file | diff | annotate |
| Thu, 26 Feb 2009 08:44:12 -0800 |
revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
|
file | diff | annotate |
| Mon, 23 Feb 2009 16:25:52 -0800 |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
file | diff | annotate |
| Fri, 20 Feb 2009 10:14:32 +0100 |
defensive implementation of pretty serialisation of lists and characters
|
file | diff | annotate |
| Mon, 16 Feb 2009 10:13:30 +0100 |
Added nitpick attribute, and fixed typo.
|
file | diff | annotate |
| Tue, 10 Feb 2009 17:53:51 -0800 |
const_name antiquotations
|
file | diff | annotate |
| Sat, 07 Feb 2009 09:57:07 +0100 |
code theorems for nth, list_update
|
file | diff | annotate |
| Sat, 07 Feb 2009 08:37:43 +0100 |
code theorems for nth, list_update
|
file | diff | annotate |
| Fri, 06 Feb 2009 15:15:27 +0100 |
authentic syntax for List.nth
|
file | diff | annotate |
| Tue, 03 Feb 2009 16:39:52 +0100 |
dropped global Nil/Append interpretation
|
file | diff | annotate |
| Mon, 26 Jan 2009 08:23:41 +0100 |
sorted_take, sorted_drop
|
file | diff | annotate |
| Fri, 16 Jan 2009 14:58:11 +0100 |
migrated class package to new locale implementation
|
file | diff | annotate |
| Wed, 31 Dec 2008 20:31:36 +0100 |
eliminated OldTerm.add_term_free_names;
|
file | diff | annotate |
| Wed, 31 Dec 2008 18:53:16 +0100 |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file | diff | annotate |
| Thu, 11 Dec 2008 18:30:26 +0100 |
Conversion of HOL-Main and ZF to new locales.
|
file | diff | annotate |
| Thu, 04 Dec 2008 14:43:33 +0100 |
cleaned up binding module and related code
|
file | diff | annotate |
| Mon, 17 Nov 2008 17:00:55 +0100 |
tuned unfold_locales invocation
|
file | diff | annotate |
| Fri, 14 Nov 2008 08:50:07 +0100 |
added length_unique operation for code generation
|
file | diff | annotate |
| Wed, 29 Oct 2008 11:33:40 +0100 |
explicit check for pattern discipline before code translation
|
file | diff | annotate |
| Wed, 22 Oct 2008 14:15:45 +0200 |
code identifier namings are no longer imperative
|
file | diff | annotate |
| Mon, 20 Oct 2008 23:52:59 +0200 |
added lemmas
|
file | diff | annotate |
| Fri, 10 Oct 2008 06:45:53 +0200 |
`code func` now just `code`
|
file | diff | annotate |
| Thu, 09 Oct 2008 08:47:27 +0200 |
established canonical argument order in SML code generators
|
file | diff | annotate |
| Tue, 07 Oct 2008 16:07:20 +0200 |
dropped superfluous if
|
file | diff | annotate |
| Fri, 26 Sep 2008 09:10:02 +0200 |
removed obsolete name convention "func"
|
file | diff | annotate |
| Thu, 25 Sep 2008 09:28:03 +0200 |
discontinued special treatment of op = vs. eq_class.eq
|
file | diff | annotate |
| Wed, 17 Sep 2008 21:27:08 +0200 |
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 |
a sophisticated char/nibble conversion combinator
|
file | diff | annotate |
| Tue, 16 Sep 2008 09:21:27 +0200 |
explicit size of characters
|
file | diff | annotate |
| Tue, 02 Sep 2008 20:38:17 +0200 |
distributed literal code generation out of central infrastructure
|
file | diff | annotate |
| Mon, 01 Sep 2008 22:10:42 +0200 |
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 |
cleaned up code generation for {.._} and {..<_}
|
file | diff | annotate |
| Mon, 01 Sep 2008 10:18:37 +0200 |
restructured code generation of literals
|
file | diff | annotate |
| Thu, 28 Aug 2008 22:09:20 +0200 |
restructured and split code serializer module
|
file | diff | annotate |
| Fri, 01 Aug 2008 12:57:50 +0200 |
made setsum executable on int.
|
file | diff | annotate |
| Tue, 29 Jul 2008 13:16:54 +0200 |
added removeAll
|
file | diff | annotate |
| Sat, 28 Jun 2008 21:21:13 +0200 |
@{lemma}: 'by' keyword;
|
file | diff | annotate |
| Thu, 26 Jun 2008 10:07:01 +0200 |
established Plain theory and image
|
file | diff | annotate |
| Tue, 10 Jun 2008 15:30:56 +0200 |
removed some dubious code lemmas
|
file | diff | annotate |
| Fri, 23 May 2008 16:41:39 +0200 |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
|
file | diff | annotate |
| Mon, 12 May 2008 22:11:06 +0200 |
Measure functions can now be declared via special rules, allowing for a
|
file | diff | annotate |
| Wed, 07 May 2008 10:56:37 +0200 |
- Explicitely applied predicate1I in a few proofs, because it is no longer
|
file | diff | annotate |
| Fri, 02 May 2008 18:01:02 +0200 |
Added documentation
|
file | diff | annotate |
| Fri, 25 Apr 2008 16:28:06 +0200 |
* New attribute "termination_simp": Simp rules for termination proofs
|
file | diff | annotate |
| Tue, 22 Apr 2008 08:33:20 +0200 |
dropped some metis calls
|
file | diff | annotate |
| Wed, 09 Apr 2008 05:30:14 +0200 |
move lemmas from Word/BinBoolList.thy to List.thy
|
file | diff | annotate |
| Sat, 29 Mar 2008 19:14:00 +0100 |
replaced 'ML_setup' by 'ML';
|
file | diff | annotate |
| Thu, 27 Mar 2008 19:04:36 +0100 |
restructuring; explicit case names for rule list_induct2
|
file | diff | annotate |
| Mon, 17 Mar 2008 18:37:00 +0100 |
removed duplicate lemmas;
|
file | diff | annotate |
| Tue, 26 Feb 2008 20:38:13 +0100 |
char and nibble are finite
|
file | diff | annotate |
| Tue, 26 Feb 2008 11:18:43 +0100 |
Added useful general lemmas from the work with the HeapMonad
|
file | diff | annotate |
| Fri, 15 Feb 2008 17:36:21 +0100 |
more lemmas
|
file | diff | annotate |
| Fri, 25 Jan 2008 14:54:44 +0100 |
dropped superfluous code theorems
|
file | diff | annotate |
| Thu, 10 Jan 2008 19:09:21 +0100 |
New interface for test data generators.
|
file | diff | annotate |
| Mon, 10 Dec 2007 11:24:03 +0100 |
swtiched ATP_Linkup and PreList in theory hierarchy
|
file | diff | annotate |
| Fri, 07 Dec 2007 15:07:59 +0100 |
instantiation target rather than legacy instance
|
file | diff | annotate |
| Thu, 06 Dec 2007 17:05:44 +0100 |
temporary code generator work arounds
|
file | diff | annotate |
| Thu, 06 Dec 2007 16:36:19 +0100 |
authentic primrec
|
file | diff | annotate |