#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
6df0c8c4 |
|
31-Oct-2017 |
haftmann <none@none> |
removed ancient nat-int transfer --HG-- extra : rebase_source : ce8f250636192c6dff622d66fb514fcc401ce0e7
|
#
151b7ea2 |
|
10-Apr-2017 |
wenzelm <none@none> |
tuned signature;
|
#
3c2b07e1 |
|
25-Sep-2016 |
haftmann <none@none> |
syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div --HG-- extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4
|
#
c8a3ab07 |
|
05-Mar-2016 |
wenzelm <none@none> |
tuned signature -- clarified modules; --HG-- rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML
|
#
48e2d74a |
|
03-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
f2ba2c03 |
|
01-Jun-2015 |
haftmann <none@none> |
separate class for division operator, with particular syntax added in more specific classes
|
#
cff2e75b |
|
08-Apr-2015 |
wenzelm <none@none> |
proper context for Object_Logic operations;
|
#
7b5a8c0d |
|
06-Apr-2015 |
wenzelm <none@none> |
local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
de3fa953 |
|
24-Jan-2015 |
wenzelm <none@none> |
tuned signature;
|
#
76c7446c |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued obsolete Output.urgent_message;
|
#
fecf4a1c |
|
01-Sep-2014 |
blanchet <none@none> |
tuned structure inclusion
|
#
55bc055b |
|
08-Apr-2014 |
wenzelm <none@none> |
more uniform ML/document antiquotations;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
d3dc194f |
|
20-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
81d6c2a2 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
d8e1a599 |
|
15-Mar-2014 |
wenzelm <none@none> |
tuned signature; eliminated clones;
|
#
538e72a6 |
|
14-Mar-2014 |
wenzelm <none@none> |
prefer more robust Synchronized.var;
|
#
67f491eb |
|
31-Jan-2014 |
blanchet <none@none> |
tuned ML file name --HG-- rename : src/HOL/Tools/Nitpick/nitpick_isar.ML => src/HOL/Tools/Nitpick/nitpick_commands.ML
|
#
bf9af491 |
|
12-Jul-2013 |
wenzelm <none@none> |
compile
|
#
e46f39e8 |
|
12-Jul-2013 |
wenzelm <none@none> |
system options for Isabelle/HOL proof tools;
|
#
963a5558 |
|
15-Feb-2013 |
haftmann <none@none> |
systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char --HG-- extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d
|
#
8e65386b |
|
14-Feb-2013 |
haftmann <none@none> |
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
|
#
cba6c4a3 |
|
13-Feb-2013 |
haftmann <none@none> |
formal cleanup of sources
|
#
703971ae |
|
19-Sep-2012 |
bulwahn <none@none> |
recording elapsed time in mutabelle for more detailed evaluation
|
#
f40e9657 |
|
24-Apr-2012 |
blanchet <none@none> |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
#
3c20f0d5 |
|
27-Feb-2012 |
wenzelm <none@none> |
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
|
#
5e2ce29b |
|
24-Feb-2012 |
blanchet <none@none> |
renamed 'try_methods' to 'try0' --HG-- rename : src/HOL/Tools/try_methods.ML => src/HOL/Tools/try0.ML
|
#
e71aab02 |
|
10-Feb-2012 |
bulwahn <none@none> |
making num_mutations a configuration that can be changed with the mutabelle bash command
|
#
680d93a7 |
|
11-Feb-2012 |
bulwahn <none@none> |
making max_mutants an option that can be changed in the Mutabelle-script
|
#
38cf3bd0 |
|
11-Feb-2012 |
bulwahn <none@none> |
increase timeout to 30 seconds; changing mutabelle script
|
#
0a404848 |
|
05-Feb-2012 |
bulwahn <none@none> |
adding some forbidden constant names for mutabelle
|
#
9f567200 |
|
05-Feb-2012 |
bulwahn <none@none> |
mutabelle ignores theorems with internal constants
|
#
52b8f28e |
|
31-Jan-2012 |
bulwahn <none@none> |
mutabelle must handle the case where quickcheck returns multiple results
|
#
9e8f43ba |
|
24-Jan-2012 |
bulwahn <none@none> |
some more constants on mutabelle's blacklist
|
#
027a97f7 |
|
23-Jan-2012 |
bulwahn <none@none> |
adding another internal constant to mutabelle's blacklust
|
#
cbce4e1d |
|
23-Jan-2012 |
bulwahn <none@none> |
adding some more forbidden constant names for the mutated conjecture generation
|
#
52a1d403 |
|
23-Jan-2012 |
bulwahn <none@none> |
more configurations to mutabelle
|
#
ba1c0b7f |
|
09-Nov-2011 |
bulwahn <none@none> |
quickcheck invocations in mutabelle must not catch codegenerator errors internally
|
#
5fb77bc3 |
|
07-Nov-2011 |
blanchet <none@none> |
revived Refute in Mutabelle
|
#
1baf1400 |
|
18-Oct-2011 |
bulwahn <none@none> |
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
|
#
68f3c8bc |
|
17-Oct-2011 |
bulwahn <none@none> |
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
|
#
1947c572 |
|
08-Sep-2011 |
krauss <none@none> |
added syntactic classes for "inf" and "sup"
|
#
c6f0818a |
|
08-Aug-2011 |
huffman <none@none> |
moved division ring stuff from Rings.thy to Fields.thy
|
#
d5b1119c |
|
18-Jul-2011 |
bulwahn <none@none> |
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
|
#
d4b730e6 |
|
08-Jun-2011 |
wenzelm <none@none> |
pervasive Output operations;
|
#
7f57a437 |
|
07-Jun-2011 |
bulwahn <none@none> |
printing environment in mutabelle's log
|
#
238f4e12 |
|
31-May-2011 |
blanchet <none@none> |
compile
|
#
be1c99ac |
|
27-May-2011 |
blanchet <none@none> |
compile
|
#
3e4271be |
|
27-May-2011 |
blanchet <none@none> |
renamed "Auto_Tools" "Try" --HG-- rename : src/Tools/auto_tools.ML => src/Tools/try.ML
|
#
cfdfcf72 |
|
20-Apr-2011 |
wenzelm <none@none> |
standardized some ML aliases;
|
#
e27c3b32 |
|
20-Apr-2011 |
bulwahn <none@none> |
adding two further code-generator internal constants to the blacklist of Mutabelle
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
e52436d1 |
|
31-Mar-2011 |
blanchet <none@none> |
added support for "dest:" to "try"
|
#
c33b2ed7 |
|
23-Mar-2011 |
bulwahn <none@none> |
adapting mutabelle; exporting more Quickcheck functions
|
#
fe49caa6 |
|
20-Mar-2011 |
wenzelm <none@none> |
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
|
#
8b04ee36 |
|
20-Mar-2011 |
wenzelm <none@none> |
structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
|
#
1b825f05 |
|
18-Mar-2011 |
blanchet <none@none> |
added "simp:", "intro:", and "elim:" to "try" command
|
#
cb9e36cf |
|
18-Mar-2011 |
bulwahn <none@none> |
adapting mutabelle
|
#
0071dfdb |
|
11-Feb-2011 |
bulwahn <none@none> |
adjusting HOL-Mutabelle to changes in quickcheck
|
#
5d5ff9e2 |
|
10-Jan-2011 |
wenzelm <none@none> |
eliminated Int.toString;
|
#
b6566386 |
|
28-Dec-2010 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
7d934596 |
|
28-Dec-2010 |
wenzelm <none@none> |
tuned comments;
|
#
4210efe1 |
|
16-Dec-2010 |
bulwahn <none@none> |
reactivating nitpick in Mutabelle
|
#
ef8c8890 |
|
10-Dec-2010 |
bulwahn <none@none> |
setting finite_type_size to 1 in mutabelle_extra
|
#
3e1c68db |
|
06-Dec-2010 |
bulwahn <none@none> |
commenting out sledgehammer_mtd in Mutabelle
|
#
f52e548e |
|
06-Dec-2010 |
bulwahn <none@none> |
adding timeout to try invocation in mutabelle
|
#
69bb2778 |
|
06-Dec-2010 |
bulwahn <none@none> |
adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
|
#
30e6e02c |
|
03-Dec-2010 |
bulwahn <none@none> |
adapting mutabelle
|
#
9edf4315 |
|
03-Dec-2010 |
bulwahn <none@none> |
adapting mutabelle
|
#
2527097a |
|
03-Dec-2010 |
blanchet <none@none> |
compile
|
#
644aabca |
|
03-Dec-2010 |
blanchet <none@none> |
run synchronous Auto Tools in parallel
|
#
14392075 |
|
22-Nov-2010 |
bulwahn <none@none> |
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
|
#
2ffb6884 |
|
05-Nov-2010 |
wenzelm <none@none> |
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
|
#
3c6a8225 |
|
02-Nov-2010 |
wenzelm <none@none> |
simplified some time constants;
|
#
015a372c |
|
29-Oct-2010 |
bulwahn <none@none> |
adapting HOL-Mutabelle to changes in quickcheck
|
#
93623054 |
|
25-Oct-2010 |
wenzelm <none@none> |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
#
89378690 |
|
20-Sep-2010 |
wenzelm <none@none> |
added XML.content_of convenience -- cover XML.body, which is the general situation;
|
#
8a52405a |
|
11-Sep-2010 |
blanchet <none@none> |
finished renaming "Auto_Counterexample" to "Auto_Tools"
|
#
de298049 |
|
09-Sep-2010 |
bulwahn <none@none> |
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
|
#
d5fed4bd |
|
05-Sep-2010 |
wenzelm <none@none> |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
#
b11705e1 |
|
28-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix equality now named HOL.eq
|
#
972f5d58 |
|
27-Aug-2010 |
haftmann <none@none> |
renamed class/constant eq to equal; tuned some instantiations
|
#
c91cbd4e |
|
27-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
#
dd7c556c |
|
08-Jul-2010 |
haftmann <none@none> |
tuned titles
|
#
f236006a |
|
08-May-2010 |
wenzelm <none@none> |
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
|
#
4549e8d1 |
|
05-May-2010 |
haftmann <none@none> |
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 =)
|
#
60d6d298 |
|
03-May-2010 |
wenzelm <none@none> |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
#
c9ced471 |
|
20-Apr-2010 |
bulwahn <none@none> |
tuning mutabelle; adding output of mutant theoryfile for interactive evaluation
|
#
c3452482 |
|
06-Mar-2010 |
wenzelm <none@none> |
modernized structure Object_Logic;
|
#
412ee4c2 |
|
02-Mar-2010 |
bulwahn <none@none> |
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
|
#
aa1bedf8 |
|
25-Feb-2010 |
bulwahn <none@none> |
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
|
#
7b862398 |
|
23-Feb-2010 |
bulwahn <none@none> |
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
|
#
364ef271 |
|
23-Feb-2010 |
bulwahn <none@none> |
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
|
#
75f69d99 |
|
10-Feb-2010 |
haftmann <none@none> |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
#
7b3a0878 |
|
28-Jan-2010 |
haftmann <none@none> |
new theory Algebras.thy for generic algebraic structures
|
#
9e216094 |
|
25-Jan-2010 |
bulwahn <none@none> |
adding Mutabelle to repository
|