| Wed, 01 Dec 2010 15:35:40 +0100 |
wenzelm |
just one HOLogic.mk_comp;
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 12:34:41 +0200 |
krauss |
consolidated tupled_lambda; moved to structure HOLogic
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 14:38:14 +0200 |
bulwahn |
changing String.literal to a type instead of a datatype
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:03:07 +0200 |
haftmann |
deglobalized named HOL constants
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:13:07 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 10:27:12 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:42 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
file |
diff |
annotate
|
| Thu, 10 Jun 2010 12:24:01 +0200 |
haftmann |
qualified type "*"; qualified constants Pair, fst, snd, split
|
file |
diff |
annotate
|
| Tue, 08 Jun 2010 16:37:19 +0200 |
haftmann |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| 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
|