wenzelm [Wed, 16 Nov 2005 17:45:22 +0100] rev 18176
Term.betapply;
paulson [Wed, 16 Nov 2005 15:29:23 +0100] rev 18175
new version of "tryres" allowing multiple unifiers (apparently needed for
Skolemization of higher-order theorems)
wenzelm [Wed, 16 Nov 2005 14:05:41 +0100] rev 18174
pgmlsymbolson: append Symbol.xsymbolsN at end!
wenzelm [Tue, 15 Nov 2005 14:08:32 +0100] rev 18173
better no -d option;
haftmann [Tue, 15 Nov 2005 10:11:52 +0100] rev 18172
added generic transformators
paulson [Mon, 14 Nov 2005 18:25:34 +0100] rev 18171
removal of is_hol
haftmann [Mon, 14 Nov 2005 16:26:40 +0100] rev 18170
added module system
haftmann [Mon, 14 Nov 2005 15:23:33 +0100] rev 18169
added modules for code generator generation two, not operational yet
haftmann [Mon, 14 Nov 2005 15:15:34 +0100] rev 18168
class_package - operational view on type classes
haftmann [Mon, 14 Nov 2005 15:15:07 +0100] rev 18167
string_of_alist - convenient q'n'd printout function
wenzelm [Mon, 14 Nov 2005 15:14:59 +0100] rev 18166
support for polyml-4.2.0;
haftmann [Mon, 14 Nov 2005 15:14:32 +0100] rev 18165
new syntax for class_package
wenzelm [Mon, 14 Nov 2005 14:37:48 +0100] rev 18164
added const_instance;
wenzelm [Mon, 14 Nov 2005 14:37:38 +0100] rev 18163
added instance;
wenzelm [Mon, 14 Nov 2005 14:37:15 +0100] rev 18162
added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
wenzelm [Mon, 14 Nov 2005 14:36:46 +0100] rev 18161
Compatibility wrapper for Poly/ML 4.2.0.
wenzelm [Mon, 14 Nov 2005 14:36:29 +0100] rev 18160
tuned;
urbanc [Mon, 14 Nov 2005 13:59:58 +0100] rev 18159
added a few equivariance lemmas (they need to be automated
eventually)
urbanc [Sun, 13 Nov 2005 22:36:30 +0100] rev 18158
changed the HOL_basic_ss back and selectively added
simp_thms and triv_forall_equality. (Otherwise the
goals would have been simplified too much)
urbanc [Sun, 13 Nov 2005 20:33:36 +0100] rev 18157
exchanged HOL_ss for HOL_basic_ss in the simplification
part. Otherwise the case where the context is instantiated
with unit leads to vacuous quantifiers, such as
ALL a. A
chaieb [Fri, 11 Nov 2005 10:50:43 +0100] rev 18156
a proof step corrected due to the changement in the presburger method.
chaieb [Fri, 11 Nov 2005 10:49:59 +0100] rev 18155
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
huffman [Fri, 11 Nov 2005 00:09:37 +0100] rev 18154
add header
wenzelm [Thu, 10 Nov 2005 21:14:05 +0100] rev 18153
tuned proofs;
wenzelm [Thu, 10 Nov 2005 20:57:22 +0100] rev 18152
moved find_free to term.ML;
wenzelm [Thu, 10 Nov 2005 20:57:21 +0100] rev 18151
guess: Seq.hd;
Term.find_free;
wenzelm [Thu, 10 Nov 2005 20:57:20 +0100] rev 18150
guess: Toplevel.proof;
wenzelm [Thu, 10 Nov 2005 20:57:19 +0100] rev 18149
added find_free (from Isar/proof_context.ML);