ran isabelle update_op on all sources

more symbols;

dedicated definition for coprimality

--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae

simplified setup

--HG--
extra : rebase_source : 3f48f5e2ae49ea17fb27eb23e2c7520bc75677a3

include GCD as integral part of computational algebra in session HOL

setsum -> sum

renamed listsum -> sum_list, listprod ~> prod_list

prefer symbols for "abs";

isabelle update_cartouches -c -t;

option "inductive_defs" controls exposure of def and mono facts;

do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';

eliminated \<Colon>;

isabelle update_cartouches;

modernized header uniformly as section;

added 'extraction' plugins -- this might help 'HOL-Proofs'

generate 'code' attribute only if 'code' plugin is enabled

disable datatype 'plugins' for internal types

updated news

use 'datatype_new' in 'Main'

tuning

tuned dependencies

reduces Sledgehammer dependencies

move size hooks together, with new one preceding old one and sharing same theory data

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

simplified data structure by reducing the incidence of clumsy indices

renamed 'nat_{case,rec}' to '{case,rec}_nat'

renamed '{prod,sum,bool,unit}_case' to 'case_...'

tuned ML file name

--HG--
rename : src/HOL/Tools/Nitpick/nitpick_isar.ML => src/HOL/Tools/Nitpick/nitpick_commands.ML

compile

adapted to move of Wfrec

rationalize imports

killed more "no_atp"s

hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);

moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong

prefer ML_file over old uses;

tuned proofs;

fixed "real" after they were redefined as a 'quotient_type'

declare command keywords via theory header, including strict checking outside Pure;

added problem importer

rebranded Nitrox, for more uniformity

--HG--
rename : src/HOL/TPTP/lib/Tools/nitrox => src/HOL/TPTP/lib/Tools/tptp_nitpick
rename : src/HOL/Tools/Nitpick/nitrox.ML => src/HOL/Tools/Nitpick/nitpick_tptp.ML

adjusted to set/pred distinction by means of type constructor `set`

bouned transitive closure

--HG--
extra : rebase_source : 3d0df473619b9c72b32a96ed4951a34dd2ad6c82

observe distinction between sets and predicates more properly

replaced Nitpick's hardwired basic_ersatz_table by context data

moved recdef package to HOL/Library/Old_Recdef.thy

--HG--
rename : src/HOL/Recdef.thy => src/HOL/Library/Old_Recdef.thy

added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter

rename Nitpick's (internal) auxiliary lemmas

renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics

remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much

fix special handling of set products

remove more clutter related to old "fast_descrs" optimization

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

remove "minipick" (the toy version of Nitpick) and some tests;
a small step towards making the Nitpick tests take less time

group record-related ML files

adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"

adjust Nitpick's handling of "<" on "rat"s and "reals"

fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option

add "no_atp"s to Nitpick lemmas

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

added support for "specification" and "ax_specification" constructs to Nitpick

improve precision of "card" in Nitpick

improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"

added "finitize" option to Nitpick + remove dependency on "Coinductive_List"

improved Nitpick's support for quotient types

enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit

added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s

more work on Nitpick's support for nonstandard models + fix in model reconstruction

various cosmetic changes to Nitpick

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

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

added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick

fix issues with previous Nitpick change

added support for binary nat/int representation to Nitpick

bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits;
the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm

tuned imports

introduced Auto Nitpick in addition to Auto Quickcheck;
this required generalizing the theorem hook used by Quickcheck,
following a suggestion by Florian

renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary

dropped obsolete comment

added Nitpick's theory and ML files to Isabelle/HOL;
the examples and the documentation are on their way.