| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 14:50:00 +0200 |
haftmann |
rudimentary code setup for set operations
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 06:51:59 +0200 |
huffman |
remove simp attribute from range_composition
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:43 +0200 |
berghofe |
- Now uses Orderings as parent theory
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:16 +0200 |
haftmann |
constant HOL.eq now qualified
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:32 +0200 |
haftmann |
explicit class "eq" for operational equality
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:47:35 +0100 |
wenzelm |
eliminated change_claset/simpset;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:15 +0100 |
haftmann |
moved some set lemmas from Set.thy here
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
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
|
| Fri, 23 Nov 2007 21:09:33 +0100 |
haftmann |
interpretation of typedecls: instantiation to class type
|
file |
diff |
annotate
|
| Fri, 09 Nov 2007 13:41:27 +0100 |
krauss |
avoid name clashes when generating code for union, inter
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 18:18:39 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 20:27:58 +0200 |
haftmann |
convenient obtain rule for sets
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 16:37:30 +0200 |
haftmann |
clarified code lemmas
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:16 +0200 |
haftmann |
made sets executable
|
file |
diff |
annotate
|
| Sun, 19 Aug 2007 21:21:37 +0200 |
nipkow |
Made UN_Un simp
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 13:58:57 +0200 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:39 +0200 |
haftmann |
updated code generator setup
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:44 +0200 |
haftmann |
code lemma for contents
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 08:27:23 +0100 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:11 +0100 |
haftmann |
added instance of sets as distributive lattices
|
file |
diff |
annotate
|