haftmann [Fri, 02 Nov 2007 18:52:58 +0100] rev 25267
proper reinitialisation after subclass
haftmann [Fri, 02 Nov 2007 18:52:57 +0100] rev 25266
clarified
paulson [Fri, 02 Nov 2007 16:38:37 +0100] rev 25265
tweaked
paulson [Fri, 02 Nov 2007 16:38:14 +0100] rev 25264
recdef to fun
nipkow [Fri, 02 Nov 2007 15:56:49 +0100] rev 25263
*** empty log message ***
kleing [Fri, 02 Nov 2007 12:35:27 +0100] rev 25262
Added reference to Jeremy Dawson's paper on the word library.
Added header to remaining word/*.thy files so they show up in toc.
nipkow [Fri, 02 Nov 2007 08:59:15 +0100] rev 25261
recdef -> fun
nipkow [Fri, 02 Nov 2007 08:26:01 +0100] rev 25260
added Fun
haftmann [Fri, 02 Nov 2007 08:17:33 +0100] rev 25259
tuned
nipkow [Thu, 01 Nov 2007 20:20:19 +0100] rev 25258
recdef -> fun
nipkow [Thu, 01 Nov 2007 13:44:44 +0100] rev 25257
*** empty log message ***
paulson [Wed, 31 Oct 2007 15:10:34 +0100] rev 25256
Catch exceptions arising during the abstraction operation.
Filter out theorems that are "too deep".
chaieb [Wed, 31 Oct 2007 12:19:45 +0100] rev 25255
Added example for the ideal membership problem solved by algebra
chaieb [Wed, 31 Oct 2007 12:19:44 +0100] rev 25254
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
chaieb [Wed, 31 Oct 2007 12:19:43 +0100] rev 25253
changed signature according to normalizer_data.ML