smolkas [Mon, 18 Feb 2013 12:16:27 +0100] rev 51179
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas [Mon, 18 Feb 2013 12:16:02 +0100] rev 51178
simplified byline, isar_qualifier
blanchet [Mon, 18 Feb 2013 11:33:43 +0100] rev 51177
tuned code: factored out parent computation
blanchet [Mon, 18 Feb 2013 10:43:36 +0100] rev 51176
tuned code
Andreas Lochbihler [Mon, 18 Feb 2013 08:52:23 +0100] rev 51175
simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay)
haftmann [Sun, 17 Feb 2013 22:56:54 +0100] rev 51174
fundamentals about discrete logarithm and square root
haftmann [Sun, 17 Feb 2013 21:29:30 +0100] rev 51173
Sieve of Eratosthenes
haftmann [Sun, 17 Feb 2013 20:45:49 +0100] rev 51172
note on parallel computation
haftmann [Sun, 17 Feb 2013 19:39:00 +0100] rev 51171
corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann [Sun, 17 Feb 2013 11:34:40 +0100] rev 51170
simplified construction of upto_aux
haftmann [Sun, 17 Feb 2013 11:06:10 +0100] rev 51169
merged
haftmann [Sat, 16 Feb 2013 08:21:08 +0100] rev 51168
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann [Sun, 17 Feb 2013 10:40:53 +0100] rev 51167
CONTRIBUTORS
nipkow [Sat, 16 Feb 2013 15:27:10 +0100] rev 51166
tail recursive code for function "upto"
blanchet [Fri, 15 Feb 2013 16:53:39 +0100] rev 51165
tuning
blanchet [Fri, 15 Feb 2013 16:40:39 +0100] rev 51164
repaired collateral damage from 4f0147ed8bcb
traytel [Fri, 15 Feb 2013 16:17:05 +0100] rev 51163
Backed out changeset: 3fe7242f8346,
many proofs (e.g. in Extended_Real and Approximation) rely on coercions not being lifted over sets
haftmann [Fri, 15 Feb 2013 12:48:20 +0100] rev 51162
dropped now obsolete hint;
a few words on theory IArray;
dropped reference to obsolete theory Efficient_Nat
haftmann [Fri, 15 Feb 2013 11:47:34 +0100] rev 51161
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary
haftmann [Fri, 15 Feb 2013 11:47:33 +0100] rev 51160
systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char
traytel [Fri, 15 Feb 2013 15:22:16 +0100] rev 51159
coercions between base types can be lifted to sets
blanchet [Fri, 15 Feb 2013 13:54:54 +0100] rev 51158
annotate obtains with types
blanchet [Fri, 15 Feb 2013 13:43:06 +0100] rev 51157
merge
blanchet [Fri, 15 Feb 2013 13:37:37 +0100] rev 51156
made check for conjecture skolemization sound