| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Fri, 22 Jan 2010 16:56:51 +0100 |
haftmann |
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 22:56:14 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 14:00:12 +0200 |
haftmann |
Code_Eval(uation)
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 20:49:53 +0200 |
krauss |
fixed HOLogic.stringT
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 15:20:57 +0200 |
haftmann |
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 13:52:17 +0200 |
haftmann |
termT and term_of_const
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 16:48:34 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 13:37:09 +0200 |
haftmann |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 08:38:57 +0200 |
haftmann |
more appropriate mk_typerep
|
file |
diff |
annotate
|
| Fri, 05 Jun 2009 09:23:41 +0200 |
haftmann |
added mk_valtermify_app and mk_random
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 15:28:59 +0200 |
haftmann |
insert now qualified and with authentic syntax
|
file |
diff |
annotate
|
| Tue, 19 May 2009 16:54:55 +0200 |
haftmann |
String.literal replaces message_string, code_numeral replaces (code_)index
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:18 +0200 |
haftmann |
combinators for single-threaded operations
|
file |
diff |
annotate
|
| Wed, 13 May 2009 18:41:38 +0200 |
haftmann |
added abstract operations for typerep/term_of
|
file |
diff |
annotate
|
| Wed, 06 May 2009 16:01:06 +0200 |
haftmann |
refined HOL string theories and corresponding ML fragments
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 16:20:07 +0100 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:56:51 +0100 |
haftmann |
HOLogic.mk_set, HOLogic.dest_set
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|