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);
wenzelm [Thu, 10 Nov 2005 20:57:18 +0100] rev 18148
curried multiply;
wenzelm [Thu, 10 Nov 2005 20:57:17 +0100] rev 18147
induct method: fixes;
tuned;
wenzelm [Thu, 10 Nov 2005 20:57:16 +0100] rev 18146
uncurried Consts.typargs;
wenzelm [Thu, 10 Nov 2005 20:57:11 +0100] rev 18145
renamed Thm.cgoal_of to Thm.cprem_of;
paulson [Thu, 10 Nov 2005 17:33:14 +0100] rev 18144
duplicate axioms in ATP linkup, and general fixes
paulson [Thu, 10 Nov 2005 17:31:44 +0100] rev 18143
tidying
urbanc [Thu, 10 Nov 2005 00:36:26 +0100] rev 18142
called the induction principle "unsafe" instead of "test".