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;