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;

tuned;

another attempt to standardize sort order in a portable way;

rebundled polyml-5.5.0-2, which now includes the sources as usual (e.q. required for formal references in Isabelle/ML);

updated for release;

tuned;

minimal updated of jEdit/README.html, without any substantial reforms;

clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally; reverted f3588e59aeaa accordingly;

avoid extra fork for fulfill_proof_future whenever possible -- without proof terms it merely doubles the number of proof tasks redundantly, by piggy-backing another 10 microseconds task;

report status more frequently on demand;

more efficient inlined properties, especially relevant for voluminous tasks trace;

more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);

repackaged polyml-5.5.0-1 -- only x86-cygwin changed;

better apply peflags at build time, to avoid antivirus getting nervous about changing executables;

Added tag Isabelle2013-RC1 for changeset 2c3d0cb151c0

tuned state display

tuned names

tuned

tuned identifier

tuned top

Typo in description of abs_def.

distinguish one more kind of proofs

added markers in proofs identifying origin of proofs, in eval driver

added option to use SNoW as machine learning algo

more robustness in Isar proof reconstruction (cf. bug report by Ondrej)

more precise error message

killed deadcode

more robustness w.r.t. 0

hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly

tuned indent

drop needless .0s

distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation

infix syntax for streams (reflecting the one for lists)

replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules

check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop

removed spurious trimming

tuned

tuned slicing (E-MaLeS and E-Par)

tune slices further

tweak ATP slices further

compile

also have SMT solvers alternate fact filter

use the right filter in each slice

tuned slices

store fact filter along with ATP slice

tuned data structure

thread through fact triple component from which used facts come, for accurate index output

more precise output of selected facts

thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices

simplified SMT solver code in Sledgehammer

eliminated needless speed optimization -- and simplified code quite a bit

distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds

report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices

remove unnecessary assumption from real_normed_vector

adapted to new MaSh interface

use order topology for extended reals

introduce order topology

simplify heine_borel type class

compute proper weight for "p proves p" in MaSh

restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual

tuned

back to post-release mode -- after fork point;

updated for release;

merged

misc tuning for release;

tuned;

accomodate scala-2.9.2;

afford parallel proof terms;

always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;

simplified proofs

tuning

misc cleanup;

tuned signature;

use inlined session name as title for charts; tuned signature;

tuned signature;

charts for future task runtime statistics;

merged

more uniform permissions;

more generous C stack size as in Linux and Mac OS X, to reduce chance of Cygwin-specific crashes; more generous initial C heap within VM; proper executable;

tuned proof -- much faster;

more systematic task statistics;

added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);

generalized diameter from real_normed_vector to metric_space

tuned proof

tune prove compact_eq_totally_bounded

generalized theorem edelstein_fix to class metric_space

tuning

pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier

optimization -- evaluate conversion to table only once

MeSh prover generation

use correct weights in MeSh driver

use precomputed MaSh/MePo data whenever available

merged

merged

copy Cygwin-Latex-Setup.bat;

more formal Cygwin-Latex-Setup (excluding bulky texlive-collection-fontsextra, which would be required for eulervm.sty);

updated to cygwin-20130117;

proper permissions;

tuned;

updated to jdk-7u11;

simplify proof of compact_imp_bounded

added step to skip some queries

provide a means to skip a method

evaluate more cases (cf. paper)

updated MaSh

make SPASS more configurable, for experiments

generalize more topology lemmas

generalize topology lemmas; simplify proofs

merged

tuned signature (again) -- keep Properties more generic;

tuned proofs;

simplified prove of compact_imp_bounded

use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma

move auxiliary lemma to top

add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite

group compactness-eq-seq-compactness lemmas together

replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy

tuned

removed subseq_bigger (replaced by seq_suble)

countablility of finite subsets and rational numbers

generalize compact_path_image to topological_space

re-generated components.sha1;

merged

more system-independent order of components.sha1 to keep changes monotonic;

clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;

delay to give users a chance to see what was happening, even with auto_close enabled;