isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

hiding randompred definitions
2009-10-27, by bulwahn
changes to example file
2009-10-27, by bulwahn
print retrieved specification when printing intermediate results
2009-10-27, by bulwahn
added option show_modes to predicate compiler
2009-10-27, by bulwahn
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
2009-10-27, by bulwahn
removed unused file smt_builtin.ML,
2009-10-27, by boehmes
included description for sledgehammer options in Mirabelle script
2009-10-27, by boehmes
measure runtime of ATPs only if requested
2009-10-27, by boehmes
eliminated some old folds;
2009-10-27, by wenzelm
eliminated some old folds;
2009-10-27, by wenzelm
Datatype.read_typ: standard argument order;
2009-10-27, by wenzelm
normalized basic type abbreviations;
2009-10-27, by wenzelm
misc tuning and simplification;
2009-10-27, by wenzelm
merged
2009-10-27, by wenzelm
merged
2009-10-27, by wenzelm
merged
2009-10-27, by haftmann
merged
2009-10-27, by haftmann
tuned
2009-10-27, by haftmann
tuned
2009-10-27, by haftmann
dropped obsolete comment
2009-10-27, by haftmann
added implode and explode
2009-10-27, by haftmann
added friendly error message when Kodkodi is not available
2009-10-27, by blanchet
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
2009-10-27, by blanchet
merged
2009-10-27, by blanchet
merged
2009-10-26, by blanchet
made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
2009-10-26, by blanchet
more thread-safe access to global refs;
2009-10-27, by wenzelm
avoid structure alias;
2009-10-27, by wenzelm
comment;
2009-10-27, by wenzelm
non-critical output -- ship message in one piece;
2009-10-27, by wenzelm
ProofContext.setmp_verbose_CRITICAL;
2009-10-27, by wenzelm
non-critical atomic accesses;
2009-10-27, by wenzelm
critical comments;
2009-10-27, by wenzelm
tuned;
2009-10-27, by wenzelm
SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;
2009-10-27, by wenzelm
max_threads_value: eliminated tested_platform -- Poly/ML 5.3 fully supports linux, darwin, solaris, cygwin;
2009-10-27, by wenzelm
lemma converse_inv_image
2009-10-26, by krauss
authentic constants; moved "acyclic" further down
2009-10-26, by krauss
point-free characterization of well-foundedness
2009-10-26, by krauss
replaced (outdated) comments by explicit statements
2009-10-26, by krauss
reactivated test on sunbroy2 -- with full proof parallelism (requires Poly/ML-SVN-921);
2009-10-26, by wenzelm
forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;
2009-10-26, by wenzelm
tuned;
2009-10-26, by wenzelm
added nitpick manual here;
2009-10-26, by wenzelm
recovered sort indentation for "sort position", as documented in the file;
2009-10-26, by wenzelm
tuned white space;
2009-10-26, by wenzelm
merged
2009-10-26, by haftmann
merged
2009-10-26, by haftmann
avoid upto if not needed
2009-10-26, by haftmann
conceal quickcheck generators
2009-10-26, by haftmann
merged
2009-10-26, by blanchet
merged
2009-10-26, by blanchet
make Nitpick compile again
2009-10-26, by blanchet
merged
2009-10-26, by blanchet
be somewhat more liberal in Nitpick about which types may occur in formulas
2009-10-23, by blanchet
make the Nitpick examples work again
2009-10-23, by blanchet
updated keyword files to include "nitpick" and "nitpick_params"
2009-10-23, by blanchet
continuation of Nitpick's integration into Isabelle;
2009-10-23, by blanchet
updated Nitpick documentation to remove weird default for "overlord"
2009-10-23, by blanchet
updated Nitpick manual to reflect the latest Stand der Dinge
2009-10-23, by blanchet
merged
2009-10-22, by blanchet
wrap line correctly in Nitpick documentation
2009-10-22, by blanchet
added Nitpick's theory and ML files to Isabelle/HOL;
2009-10-22, by blanchet
Added Nitpick manual.
2009-10-22, by blanchet
merged
2009-10-26, by berghofe
Added Pattern.thy to Nominal/Examples.
2009-10-26, by berghofe
merged
2009-10-26, by haftmann
tuned
2009-10-26, by haftmann
added SML_Quickcheck import
2009-10-26, by haftmann
tuned code setup for primitive boolean connectors
2009-10-26, by haftmann
legacy warnings for old-style term styles
2009-10-26, by haftmann
removed unnecessary NameSpace prefix;
2009-10-26, by wenzelm
misc tuning and updates;
2009-10-26, by wenzelm
merged
2009-10-26, by wenzelm
implicit default is 4 cores -- more cost-effective;
2009-10-26, by wenzelm
deleted junk;
2009-10-26, by wenzelm
more precise dependencies, notably for HOL-Multivariate_Analysis;
2009-10-26, by wenzelm
re-moved theory Fin_Fun to AFP
2009-10-26, by haftmann
merged
2009-10-26, by haftmann
distinguished session for multivariate analysis
2009-10-23, by himmelma
adjusted to changes in corresponding ML code
2009-10-26, by haftmann
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25, by wenzelm
maintain theory name via name space, not tags;
2009-10-25, by wenzelm
name space groups are identified by serial, not serial_string;
2009-10-25, by wenzelm
maintain group via name space, not tags;
2009-10-25, by wenzelm
LocalTheory.naming_of;
2009-10-25, by wenzelm
begin_theory: set theory_name here;
2009-10-25, by wenzelm
maintain group via name space, not tags;
2009-10-25, by wenzelm
maintain proper Name_Space.naming, with conceal and set_group;
2009-10-25, by wenzelm
more direct access to naming;
2009-10-25, by wenzelm
Name_Space.naming: maintain group and theory_name as well;
2009-10-25, by wenzelm
export is_concealed;
2009-10-25, by wenzelm
merge_list: no exception DUP here;
2009-10-25, by wenzelm
merged
2009-10-25, by wenzelm
more uniform ISABELLE_USEDIR_OPTIONS;
2009-10-25, by wenzelm
make SML/NJ happy;
2009-10-25, by wenzelm
conceal consts via name space, not tags;
2009-10-25, by wenzelm
allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-25, by wenzelm
switch to polyml-5.2.1 to see if it impacts performance;
2009-10-25, by wenzelm
merged
2009-10-25, by chaieb
Multivariate polynomials library over fields
2009-10-25, by chaieb
A theory of polynomials based on lists
2009-10-25, by chaieb
Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
2009-10-25, by chaieb
merged
2009-10-25, by wenzelm
further changes due to the previous merge in the predicate compiler
2009-10-24, by bulwahn
merge -- imported from bulwahn d759e2728188;
2009-10-24, by wenzelm
removed tuple functions from the predicate compiler
2009-10-24, by bulwahn
improving the compilation with higher-order arguments in the predicate compiler
2009-10-24, by bulwahn
now the predicate compilere handles the predicate without introduction rules better as before
2009-10-24, by bulwahn
removed dead code; added examples
2009-10-24, by bulwahn
removed obsolete GeneratorPrem; clean-up after modularization; tuned
2009-10-24, by bulwahn
modularized the compilation in the predicate compiler
2009-10-24, by bulwahn
adapted parser for options in the predicate compiler
2009-10-24, by bulwahn
modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples
2009-10-24, by bulwahn
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
2009-10-24, by bulwahn
added skip_proof option; playing with compilation of depth-limited predicates
2009-10-24, by bulwahn
reinvestigating the compilation of the random computation in the predicate compiler
2009-10-24, by bulwahn
added option to generate random values to values command in the predicate compiler
2009-10-24, by bulwahn
commented out the random generator compilation in the example file
2009-10-24, by bulwahn
added option to execute depth-limited computations for the values command in the predicate compiler
2009-10-24, by bulwahn