isabelle update -u control_cartouches;

removed ancient nat-int transfer

--HG--
extra : rebase_source : ce8f250636192c6dff622d66fb514fcc401ce0e7

tuned signature;

syntactic type class for operation mod named after mod;
simplified assumptions of type class semiring_div

--HG--
extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4

tuned signature -- clarified modules;

--HG--
rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML

tuned signature;

separate class for division operator, with particular syntax added in more specific classes

proper context for Object_Logic operations;

local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned signature -- prefer qualified names;

tuned signature;

discontinued obsolete Output.urgent_message;

tuned structure inclusion

more uniform ML/document antiquotations;

more qualified names;

more qualified names;

more qualified names;

tuned signature;
eliminated clones;

prefer more robust Synchronized.var;

tuned ML file name

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

compile

system options for Isabelle/HOL proof tools;

systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char

--HG--
extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d

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

--HG--
rename : src/HOL/DSequence.thy => src/HOL/Limited_Sequence.thy
rename : src/HOL/Quickcheck.thy => src/HOL/Quickcheck_Random.thy
extra : rebase_source : b6adaac1637d6d1cc809d2f937ae890fcc21969c

formal cleanup of sources

recording elapsed time in mutabelle for more detailed evaluation

handle TPTP definitions as definitions in Nitpick rather than as axioms

merged fork with new numeral representation (see NEWS)

more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);

renamed 'try_methods' to 'try0'

--HG--
rename : src/HOL/Tools/try_methods.ML => src/HOL/Tools/try0.ML

making num_mutations a configuration that can be changed with the mutabelle bash command

making max_mutants an option that can be changed in the Mutabelle-script

increase timeout to 30 seconds; changing mutabelle script

adding some forbidden constant names for mutabelle

mutabelle ignores theorems with internal constants

mutabelle must handle the case where quickcheck returns multiple results

some more constants on mutabelle's blacklist

adding another internal constant to mutabelle's blacklust

adding some more forbidden constant names for the mutated conjecture generation

more configurations to mutabelle

quickcheck invocations in mutabelle must not catch codegenerator errors internally

revived Refute in Mutabelle

adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra

moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms

added syntactic classes for "inf" and "sup"

moved division ring stuff from Rings.thy to Fields.thy

adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle

pervasive Output operations;

printing environment in mutabelle's log

compile

compile

renamed "Auto_Tools" "Try"

--HG--
rename : src/Tools/auto_tools.ML => src/Tools/try.ML

standardized some ML aliases;

adding two further code-generator internal constants to the blacklist of Mutabelle

modernized structure Proof_Context;

added support for "dest:" to "try"

adapting mutabelle; exporting more Quickcheck functions

simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);

structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;

added "simp:", "intro:", and "elim:" to "try" command

adapting mutabelle

adjusting HOL-Mutabelle to changes in quickcheck

eliminated Int.toString;

made SML/NJ happy;

tuned comments;

reactivating nitpick in Mutabelle

setting finite_type_size to 1 in mutabelle_extra

commenting out sledgehammer_mtd in Mutabelle

adding timeout to try invocation in mutabelle

adding filtering, sytactic welltyping, and sledgehammer method in mutabelle

adapting mutabelle

adapting mutabelle

compile

run synchronous Auto Tools in parallel

adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle

explicit indication of some remaining violations of the Isabelle/ML interrupt model;

simplified some time constants;

adapting HOL-Mutabelle to changes in quickcheck

renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;

added XML.content_of convenience -- cover XML.body, which is the general situation;

finished renaming "Auto_Counterexample" to "Auto_Tools"

removing report from the arguments of the quickcheck functions and refering to it by picking it from the context

pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

formerly unnamed infix equality now named HOL.eq

renamed class/constant eq to equal; tuned some instantiations

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

tuned titles

prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

tuning mutabelle; adding output of mutant theoryfile for interactive evaluation

modernized structure Object_Logic;

adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck

adopting Mutabelle to quickcheck reporting; improving quickcheck reporting

adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session

adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening

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

new theory Algebras.thy for generic algebraic structures

adding Mutabelle to repository