syntactic improvements and tuning names in the code generator due to Florian's code review

match types when applying mono_thm -- previous export generalizes type variables; added trivial regression test

fixed headers;

less ambiguous syntax;

tuned proofs;

merged

catch PatternMatchFail exceptions in narrowing-based quickcheck

removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition

ensuring that some constants are generated in the source code by adding calls in ensure_testable

adding abstraction layer; more precise function names

adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used

determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations

only annotating constants with sort constraints

also adding type annotations for the dynamic invocation

removed legacy lemmas in Complete_Lattices

increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling

more isatest stats;

refined Symbol.is_symbolic -- cover recoded versions as well;

double clicks switch to document node buffer;

tuned;

explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);

at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;

instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);

unique file names via serial numbers, to allow files like "root" or multiple files with same base name;

imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;

merged

numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else

removed obsolete patches for PG 4.1;

additional space for borderless UI;

more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);

explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;

isatest settings for macbroy6 (Mac OS X Lion);

more Mac OS reference hardware;

updated to SML/NJ 110.73;

tentative announcement based on current NEWS;

tuned;

separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);

updated for release;

tuned;

updated generated file;

updated Complete_Lattices;

some tuning and re-ordering for release;

misc tuning for release;

more contributors;

tuned proofs;

tweak keyboard shortcuts for Mac OS X;

explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;

finite sequences as useful as introductory example;

discontinued hard-wired JAVA_HOME treatment for Mac OS X (cf. f471a2fb9a95), which can cause confusions of "isabelle java" vs. "isabelle scala" -- moved settings to external component;

graph traversal in topological order; Session.snapshot() with sensible defaults;

Document.Node.Name convenience;

more precise painting;

more elaborate Node_Renderer, which paints node_name.theory only;

raised default log level -- to avoid confusing warning about scala.tools.nsc.plugins.Plugin, which is mistaken as jEdit plugin;

tuned signature;

more careful traversal of theory dependencies to retain standard import order;

sane default for class Thy_Load;

removed obsolete patches for PG 4.1;

specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;

added "isabelle scalac" convenience;

Symbol.explode as in ML;

ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;

dropped unused argument – avoids problem with SML/NJ

tuned spacing

tuned

tuned post fixpoint setup

merged

when applying induction rules, remove names of assumptions that come with the rule in case the rule is transformed by the simplifier due to instantiations

remove stray "using [[simp_trace]]"

tune indenting

removed unused legacy lemma names, some comment cleanup.

removed word_neq_0_conv from simpset, it's almost never wanted.

removed further legacy rules from Complete_Lattices

NEWS on Complete_Lattices, Lattices

tail recursive proof preprocessing (needed for huge proofs)

tuning

merged

revised AbsInt and added widening and narrowing

updated comment

updated generated code

tuned

renamed Complete_Lattices lemmas, removed legacy names

merged

create central list for language extensions used by the haskell code generator

observe distinction between sets and predicates

merged

cleand up AbsInt fixpoint iteration; tuned syntax

tuned proofs

tuned proofs

remove some redundant [simp] declarations; simplify some proofs;

tune proofs

tune simpset for Complete_Lattices

merged

added lemma motivated by a more specific lemma in the AFP-KBPs theories

simplified unsound proof detection by removing impossible case

correcting NEWS

correcting theory name and dependencies

renamed AList_Impl to AList

fastsimp -> fastforce in doc

fix typo

shorten proof of frontier_straddle

NEWS and CONTRIBUTORS

remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def

simplify proofs using LIMSEQ lemmas

remove trivial lemma Lim_at_iff_LIM

fix typos

NEWS for euclidean_space class

move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy

adding NEWS and CONTRIBUTORS

merged

correcting imports after splitting and renaming AssocList

tuned

moving connection of association lists to Mappings into a separate theory

adding NEWS and CONTRIBUTORS

tuned some symbol that probably went there by some strange encoding issue

added my contributions to NEWS and CONTRIBUTORS

fixed type intersection (again)

consistent option naming

NEWS fastsimp -> fastforce

new fastforce replacing fastsimp - less confusing name