modernized translations; formal markup of @{syntax_const} and @{const_syntax};

numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};

added ML antiquotation @{syntax_const};

treat inner token markers as syntax consts;

modernized syntax/translations;

modernized syntax/translations; tuned headers;

modernized translations;

merged

use full paths when importing theories

merged

inductive vs inductive_set explanation

modernized translations;

modernized translations;

renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;

merged

Fixed bug in code for guessing the name of the variable representing the freshness context.

dropped last occurence of the linlinordered accident

dropped Id

minor metis proof tuning

merged

NEWS

moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy

revert uninspired Structure_Syntax experiment

moved lemma field_le_epsilon from Real.thy to Fields.thy

merged

unset KODKODI explicitly -- apparently isatest patches settings cumulatively;

make Nitpick test a bit weaker; this should solve failure observed last night on "mac-poly"

merged

moved constants inverse and divide to Ring.thy

moved constants inverse and divide to Ring.thy

division ring assumes divide_inverse

rely less on ordered rewriting

merged

merged

merged (manual for "nitpick_hol.ML" and "kodkod.ML")

optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers

make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick

added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability

handle Nitpick's nonstandard model enumeration in a cleaner way; and renumber the atoms so that we get more often a_1 and a_2 and less often a_{n-1} and a_{n-2} in counterexamples

proper quoting of file paths when invoking Kodkodi from Nitpick

merged

optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil"; this gains one cardinality in the AA tree examples in the Nitpick manual

adapted example following previous Nitpick change and fixed minor optimization in Nitpick

split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come

removed obsolete CVS Ids;

modernized translations;

modernized syntax translations, using mostly abbreviation/notation; minor tuning;

simple proofs make life faster and easier

merged

hide fact names clashing with fact names from Group.thy

dropped lemma duplicates

isatest: activated HOL-Nitpick_Examples (by adding component kodkodi) on some platforms where it mostly works as expected;

adjusted to cs. 9f841f20dca6

merged

correct definedness side conditions for copy_apps and take_apps

handle case where copy_stricts cannot be proven; rewrite proof script for take_apps

rewrite proof script for take_stricts

remove redundant theorem attributes

add lemma iterate_below_fix

modernized some syntax translations;

more precise dependencies;

merged

re-generated certificates

renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields

tuned spelling

tuned proofs

hide fact Nat.add_0_right; make add_0_right from Groups priority

tuned header

using code antiquotation

tuned header

dropped accidental duplication of "lin" prefix from cs. 108662d50512

NEWS: ax_simps

avoid upto in generated code (is infix operator in library.ML)

separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4

merged

more precise proofs

moved auxiliary lemmas to more appropriate places

separate library theory for type classes combining lattices with various algebraic structures; more simp rules

dropped instantiations for combined lattices

added lemmas involving Min, Max, uminus

tuned proof

separate library theory for type classes combining lattices with various algebraic structures

more quotes;

merged

separate theory for index structures

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration

split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts, modernized perl scripts: prefer standalone executables

removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?);

modernized perl scripts: prefer standalone executables; exec bash wrapper script directly -- avoid intermediate process;

modernized perl scripts: prefer standalone executables;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

prefer explicit @{lemma} over adhoc forward reasoning;

simplified interface for ML antiquotations, struct_name is always "Isabelle";

tuned isatest ML_OPTIONS;

removed ever experimental support for Moscow ML -- hardly works anymore;

result: Single_Assignment.var;

removed slightly adhoc single-assignment feature, cf. structure Single_Assignment; access: uninterruptible update/broadcast, to prevent lost signals;

explicit representation of single-assignment variables;

fixed spelling;

removed unused "boundary" of Table/Graph.get_first;

proper treatment of paths passed to the shell -- to allow spaces in file names as usual;

renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;

misc tuning;

merged

adjusted to changeset 118b41bba42b5

tuned font handling; explicit workaround for Apple's font manager in Java 1.6, which fails to create "IsabelleTextBold" as family member of "IsabelleText";

updated versions of requirements;

filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);

eliminated self intersection and non-integer coordinates;

try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;

updated generated files;

merged

Changed 'bounded unique existential quantifiers' from a constant to syntax translation.

four changes to Nitpick: 1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems 2. do eta-contraction in the monotonicity check 3. improved quantifier massaging algorithms using ideas from Paradox 4. repaired "check_potential" and "check_genuine"

capture error messages (of SMT solvers)

updated dependencies

merged

updated SMT certificates