fundamentals about discrete logarithm and square root

Sieve of Eratosthenes

note on parallel computation

corrected and clarified Code_Binary_Nat vs. Code_Target_Nat

simplified construction of upto_aux

merged

restored proper order of NEWS entries (lost due too long-waiting patches)

CONTRIBUTORS

tail recursive code for function "upto"

tuning

repaired collateral damage from 4f0147ed8bcb

Backed out changeset: 3fe7242f8346, many proofs (e.g. in Extended_Real and Approximation) rely on coercions not being lifted over sets

dropped now obsolete hint; a few words on theory IArray; dropped reference to obsolete theory Efficient_Nat

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

systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char

coercions between base types can be lifted to sets

annotate obtains with types

merge

made check for conjecture skolemization sound

use safe var index

merged

more type class instances for Numeral_Type (contributed by Jesus Aransay)

added lemma

merge

merge

skolemize conjecture properly in Isar proof

tuning -- refactoring in preparation for handling skolemization of conjecture

removed dead weight from data structure

tuned code

tuned code

less customary term_of conversions; spurious side effect on method reflection

two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one

explicit code equation for integer_of_nat

extended stream library

merged

partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code; provide better error messages instead for card and subseteq

killed legacy alias

updated news

avoid crude/wrong theorem comparision

tuned code

more MaSh tracing

tuning

fixed metis_steps_total - was off by one

preplay subblocks

renamed sledgehammer_shrink to sledgehammer_compress

dont skolemize conjecture

introduced subblock in isar_step datatype for conjecture herbrandization

write_pdf for JFreeChart;

reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck

merged

instantiate finite_UNIV and card_UNIV for finfun type

merged

more parallel proofs in 'nominal_datatype', although sequential dark matter remains;

tuned proof;

obsolete;

tuned proofs;

tuned signature -- legacy packages might want to fork proofs as well;

merged

implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug

consolidation of library theories on product orders

type lifting setup for code numeral types

factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions

abandoned theory Plain

tuned;

clarified default according to etc/options;

Java assumes regular "re-parenting" window manager;

merged

complete metric for formal power series

eliminated union_closed_basis; cleanup Fin_Map

fine grained instantiations

use maximum norm for type finmap

generalized

generalized

merged

discontinued home-made sharing for proof terms -- leave memory management to the Poly/ML RTS;

more thorough error handling of load/save (see also c1be3072ea8f);

file system operations for Graphics2D output;

updated isabelle-release URLs;

combinator List.those; simprule for case distinction on Option.map expression

explicit conversion integer_of_nat already in Code_Numeral_Types; tuned code postprocessor setup: present arithmetic results as plain numerals without conversions

IArray ignorant of particular representation of nat

tuned, particulary name

formal cleanup of sources

another attempt for a uniform abort on code generation errors

tuned spelling

removed obsolete RC tags;

merged;

detect more hosts;

Added tag Isabelle2013 for changeset d90218288d51

make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;

merged

avoid crash (NPE) when properties are changed during prover startup (e.g. by font scaling);

updated PIDE notes;

proper root for document variants (cf. be8002ee43d8);

Added tag Isabelle2013-RC3 for changeset 8cf38c6b33f8

proforma update to jdk-7u13 -- barely relevant security updates by Oracle;

more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;

documentation for 'print_rules';

no choice of target directory -- default file permissions outside user directory tend to be ill-defined for Cygwin;

merged

provide jdk-7u13 (still inactive, potentially pointless);

allow relative directory;

standardized isabelle-server.in.tum.de;

some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);

made SML/NJ happy

more portable alternative shortcuts on numeric keypad;

more generic reference to polyml component;

Added tag Isabelle2013-RC2 for changeset 7fc61bfb1c2d

updated to polyml-5.5.0-3 based on fixes-5.5 version 1658, which provides important improvements;

merged

separate makedist_bundle for each platform family, which is more useful for manual use;

tuned;

tuned;

notes on building Poly/ML;

tuned ML platform fallback;

manual update of sessions, based on "isabelle build -nvc";

some updates concerning Proof General;

updated explanations of document preparation;

clarified NEWS on isabelle build and mkroot;

some explanations of important build options; tuned;