isabelle: Graph

added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2011-03-24, by wenzelm
more direct loose_bvar1;
2011-03-24, by wenzelm
indentation;
2011-03-24, by wenzelm
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
2011-03-24, by wenzelm
added editor mode line;
2011-03-23, by wenzelm
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
2011-03-23, by wenzelm
list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin;
2011-03-23, by wenzelm
updated contributed components
2011-03-23, by boehmes
Z3 non-commercial usage may explicitly be declined
2011-03-23, by boehmes
export status function to query whether Z3 has been activated for usage within Isabelle
2011-03-23, by boehmes
merge
2011-03-23, by blanchet
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
2011-03-23, by blanchet
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
2011-03-23, by blanchet
really be quiet
2011-03-23, by boehmes
replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
2011-03-23, by krauss
merged
2011-03-22, by wenzelm
standardized headers
2011-03-22, by hoelzl
generalized Caratheodory from algebra to ring_of_sets
2011-03-22, by hoelzl
add ring_of_sets and subset_class as basis for algebra
2011-03-22, by hoelzl
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
2011-03-22, by blanchet
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
2011-03-22, by blanchet
remove lie from documentation
2011-03-22, by blanchet
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
2011-03-22, by blanchet
make Minimizer honor "verbose" and "debug" options better
2011-03-22, by blanchet
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
2011-03-22, by nipkow
moved some configurations to AFP, and fixed others
2011-03-21, by krauss
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-22, by wenzelm
enable inner syntax source positions by default (controlled via configuration option);
2011-03-22, by wenzelm
binder_tr: more informative exception;
2011-03-22, by wenzelm
Hoare syntax: strip positions where they crash translation functions;
2011-03-22, by wenzelm
update_name_tr: more precise handling of explicit constraints, including positions;
2011-03-22, by wenzelm
statespace syntax: strip positions -- type constraints are unexpected here;
2011-03-22, by wenzelm
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
2011-03-22, by wenzelm
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
2011-03-22, by wenzelm
tuned indendation and parentheses;
2011-03-22, by wenzelm
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
2011-03-22, by wenzelm
pretty_string: proper handling of negative max_len;
2011-03-22, by wenzelm
added Lexicon.encode_position, Lexicon.decode_position;
2011-03-21, by wenzelm
tuned;
2011-03-21, by wenzelm
tuned;
2011-03-21, by wenzelm
clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
2011-03-21, by wenzelm
tuned;
2011-03-21, by wenzelm
merged
2011-03-21, by wenzelm
added judgement day configurations
2011-03-21, by krauss
another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
2011-03-21, by wenzelm
fixed perl error
2011-03-21, by krauss
eliminated unnecessary generated ROOT.ML
2011-03-21, by krauss
more precise dependencies
2011-03-21, by krauss
small test case for main mirabelle functionality, which easily breaks without noticing
2011-03-21, by krauss
propagate mirabelle failures properly;
2011-03-21, by krauss
mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
2011-03-21, by krauss
merged
2011-03-21, by bulwahn
adapting predicate_compile_quickcheck; tuned
2011-03-18, by bulwahn
adapting mutabelle
2011-03-18, by bulwahn
adapting SML_Quickcheck
2011-03-18, by bulwahn
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
2011-03-18, by bulwahn
extending the test data generators to take the evaluation terms as arguments
2011-03-18, by bulwahn
adding option of evaluating terms after invocation in quickcheck
2011-03-18, by bulwahn
adding eval option to quickcheck
2011-03-18, by bulwahn
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
2011-03-18, by bulwahn
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
2011-03-18, by bulwahn
adding a simple datatype for representing functions in Quickcheck_Narrowing
2011-03-18, by bulwahn
extending code_int type more; adding narrowing instance for type int; added test case for int instance
2011-03-18, by bulwahn
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
2011-03-18, by bulwahn
adding size as static argument in quickcheck_narrowing compilation
2011-03-18, by bulwahn
modernized specifications;
2011-03-20, by wenzelm
dropped unused structure aliases;
2011-03-20, by wenzelm
tuned;
2011-03-20, by wenzelm
NEWS: structure Timing provides various operations for timing;
2011-03-20, by wenzelm
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
2011-03-20, by wenzelm
pure Timing.timing, without any exception handling;
2011-03-20, by wenzelm
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2011-03-20, by wenzelm
pervasive cond_timeit;
2011-03-20, by wenzelm
eliminated dead code;
2011-03-20, by wenzelm
parallel preparation of document variants, within separate directories;
2011-03-20, by wenzelm
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
2011-03-20, by wenzelm
eliminated redundant doc_prefix1;
2011-03-20, by wenzelm
renamed doc_prefix2 to dump_prefix;
2011-03-20, by wenzelm
tuned;
2011-03-20, by wenzelm
tuned terminology for document variants;
2011-03-20, by wenzelm
replaced File.check by specific File.check_file, File.check_dir;
2011-03-20, by wenzelm
tuned;
2011-03-20, by wenzelm
preencode value of "need" selectors in Kodkod bounds as an optimization
2011-03-19, by blanchet
ignore "need" axioms for "nat"-like types
2011-03-19, by blanchet
added "simp:", "intro:", and "elim:" to "try" command
2011-03-18, by blanchet
optimize Kodkod axioms further w.r.t. "need" option
2011-03-18, by blanchet
optimize Kodkod bounds of nat-like datatypes
2011-03-18, by blanchet
more optimizations of bounds for "need"
2011-03-18, by blanchet
optimize Kodkod bounds when "need" is specified
2011-03-18, by blanchet
always destroy constructor patterns, since this seems to be always useful
2011-03-18, by blanchet
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
2011-03-17, by blanchet
reword Nitpick's wording concerning potential counterexamples
2011-03-17, by blanchet
prevent an exception if "card" is empty (e.g., "nitpick [card]")
2011-03-17, by blanchet
add option to function to keep trivial ATP formulas, needed for some experiments
2011-03-17, by blanchet
add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
2011-03-17, by blanchet
tuned lemma
2011-03-17, by nipkow
added lemmas
2011-03-16, by nipkow
added lemma
2011-03-15, by nipkow
support non-ground "need" values
2011-03-15, by blanchet
recover Isabelle symlink for public distribution, notably website;
2011-03-15, by wenzelm
standardized headers;
2011-03-14, by wenzelm
merged
2011-03-14, by hoelzl
reworked Probability theory: measures are not type restricted to positive extended reals
2011-03-14, by hoelzl
split Extended_Reals into parts for Library and Multivariate_Analysis
2011-03-14, by hoelzl
lemmas about addition, SUP on countable sets and infinite sums for extreal
2011-03-14, by hoelzl
add infinite sums and power on extreal
2011-03-14, by hoelzl
introduce setsum on extreal
2011-03-14, by hoelzl
use abs_extreal
2011-03-14, by hoelzl
simplified definition of open_extreal
2011-03-14, by hoelzl
use case_product for extrel[2,3]_cases
2011-03-14, by hoelzl
add Extended_Reals from AFP/Lower_Semicontinuous
2011-03-14, by hoelzl
add lemmas for monotone sequences
2011-03-14, by hoelzl
add lemmas for SUP and INF
2011-03-14, by hoelzl
generalize infinite sums
2011-03-14, by hoelzl
moved t2_spaces to HOL image
2011-03-14, by hoelzl
example settings for ISABELLE_GHC, ISABELLE_OCAML, ISABELLE_SWIPL;
2011-03-14, by wenzelm
isatest: fresh copy of settings avoids odd cumulative environment;
2011-03-14, by wenzelm
tuned exhaustive_generators
2011-03-14, by bulwahn
removing definition of cons0; hiding constants in Quickcheck_Narrowing
2011-03-14, by bulwahn
tuned subsubsection names in Quickcheck_Narrowing
2011-03-14, by bulwahn
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
2011-03-14, by bulwahn
correcting names in Narrowing_Engine and example theory for Quickcheck_Narrowing
2011-03-14, by bulwahn
renaming series and serial to narrowing in Quickcheck_Narrowing
2011-03-14, by bulwahn
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
2011-03-13, by wenzelm
tuned headers;
2011-03-13, by wenzelm
eliminated hard tabs;
2011-03-13, by wenzelm
less ambitious isatest;
2011-03-13, by wenzelm
modernized imports (untested!?);
2011-03-13, by wenzelm
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
2011-03-13, by wenzelm
explicit type SHA1.digest;
2011-03-13, by wenzelm
slightly more robust bash exec, which fails on empty executable;
2011-03-13, by wenzelm
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
2011-03-13, by wenzelm
some cleanup of old-style settings;
2011-03-13, by wenzelm
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
2011-03-13, by wenzelm
more conventional Mutabelle settings -- similar to Mirabelle;
2011-03-13, by wenzelm
more basic use of Path.position/File.read;
2011-03-13, by wenzelm
prefer qualified ISABELLE_NEOS_SERVER;
2011-03-13, by wenzelm
proper File.shell_path;
2011-03-13, by wenzelm
more conventional variable name;
2011-03-13, by wenzelm
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-03-13, by wenzelm
fixed document;
2011-03-13, by wenzelm
isatest: test more external code;
2011-03-13, by wenzelm
tuned headers;
2011-03-13, by wenzelm
allow spaces in executable names;
2011-03-13, by wenzelm
tuned;
2011-03-13, by wenzelm
tuned headers;
2011-03-13, by wenzelm
adapting example file to renaming of the quickcheck tester
2011-03-11, by bulwahn
renaming tester from lazy_exhaustive to narrowing
2011-03-11, by bulwahn
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
2011-03-11, by bulwahn
renaming example file correctly
2011-03-11, by bulwahn
adapting Main file generation for Quickcheck_Narrowing
2011-03-11, by bulwahn
adapting Quickcheck_Narrowing and example file to new names
2011-03-11, by bulwahn
renaming LSC_Examples theory to Quickcheck_Narrowing
2011-03-11, by bulwahn
renaming lazysmallcheck ML file to Quickcheck_Narrowing
2011-03-11, by bulwahn
renaming LSC to Quickcheck_Narrowing
2011-03-11, by bulwahn
adaptions in generators using the common functions
2011-03-11, by bulwahn
adding file quickcheck_common to carry common functions of all quickcheck generators
2011-03-11, by bulwahn
adapting record package to renaming of quickcheck's structures
2011-03-11, by bulwahn
moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better
2011-03-11, by bulwahn
correcting dependencies in IsaMakefile
2011-03-11, by bulwahn
renaming signatures and structures; correcting header
2011-03-11, by bulwahn
adapting Quickcheck theory after moving ML files
2011-03-11, by bulwahn
moving quickcheck_generators.ML to Quickcheck directory and renaming it random_generators.ML
2011-03-11, by bulwahn
moving exhaustive_generators.ML to Quickcheck directory
2011-03-11, by bulwahn
correcting dependencies after renaming
2011-03-11, by bulwahn
replacing naming of small by exhaustive
2011-03-11, by bulwahn
renaming smallvalue_generators.ML to exhaustive_generators.ML
2011-03-11, by bulwahn
renaming constants in Quickcheck_Exhaustive theory
2011-03-11, by bulwahn
renaming Smallcheck to Quickcheck_Exhaustive
2011-03-11, by bulwahn
only testing theory LSC_Examples when GHC is installed on the machine
2011-03-11, by bulwahn
increasing timeout of example for counterexample generation
2011-03-11, by bulwahn
adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
2011-03-11, by bulwahn
adding lazysmallcheck example theory to HOL-ex session
2011-03-11, by bulwahn
adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies
2011-03-11, by bulwahn
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
2011-03-11, by bulwahn
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
2011-03-11, by bulwahn
adding an example theory for Lazysmallcheck prototype
2011-03-11, by bulwahn
adding Lazysmallcheck prototype to HOL-Library
2011-03-11, by bulwahn
adding files for prototype of lazysmallcheck
2011-03-11, by bulwahn
removing debug message in quickcheck's postprocessor
2011-03-11, by bulwahn
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
2011-03-11, by bulwahn
renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck
2011-03-11, by bulwahn
improving term postprocessing for counterexample presentation in quickcheck
2011-03-11, by bulwahn
tuned
2011-03-11, by bulwahn
finished and tested Z3 proof reconstruction for injective functions;
2011-03-09, by boehmes
improved formula for specialization, to prevent needless specializations -- and removed dead code
2011-03-09, by blanchet
perform no arity check in debug mode so that we get to see the Kodkod problem
2011-03-09, by blanchet
spark_end now joins proofs of VCs before writing *.prv file.
2011-03-04, by berghofe
clarified
2011-03-04, by krauss
produce helpful mira summary for more errors
2011-03-04, by krauss
eliminated prems;
2011-03-04, by wenzelm
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
2011-03-03, by wenzelm
tuned proofs -- eliminated prems;
2011-03-03, by wenzelm
merged
2011-03-03, by wenzelm
merged
2011-03-03, by blanchet
don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
2011-03-03, by blanchet
simplified Thy_Info.check_file -- discontinued load path;
2011-03-03, by wenzelm
discontinued legacy load path;
2011-03-03, by wenzelm
re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;
2011-03-03, by wenzelm
modernized imports;
2011-03-03, by wenzelm
observe standard header format;
2011-03-03, by wenzelm
removed spurious 'unused_thms' (cf. 1a65b780bd56);
2011-03-03, by wenzelm
isatest cygwin-poly-e: new memory management of polyml-svn could be more stable;
2011-03-03, by wenzelm
merged
2011-03-03, by berghofe
merged
2011-03-03, by berghofe
- Made sure that sort_defs is aware of constants introduced by add_type_def
2011-03-03, by berghofe
mention new Nitpick options
2011-03-03, by blanchet
simplify "need" option's syntax
2011-03-03, by blanchet
renamed "preconstr" option "need"
2011-03-03, by blanchet
finally remove upper_bound_finite_set
2011-03-03, by hoelzl
separate settings for afp test
2011-03-03, by kleing
added missing spaces in output
2011-03-02, by blanchet
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
2011-03-02, by blanchet
unfold definitions in "preconstrs" option
2011-03-02, by blanchet
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
2011-03-02, by blanchet
make "preconstr" option more robust -- shouldn't throw exceptions
2011-03-02, by blanchet
merged
2011-03-01, by paulson
merged
2011-02-28, by paulson
declare ext [intro]: Extensionality now available by default
2011-02-28, by paulson
merged
2011-02-28, by boehmes
removed dependency on Dense_Linear_Order
2011-02-28, by boehmes
adding function Quickcheck.test_terms to provide checking a batch of terms
2011-02-28, by bulwahn
adding a function to compile a batch of terms for quickcheck with one code generation invocation
2011-02-28, by bulwahn
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
2011-02-28, by blanchet
made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
2011-02-28, by blanchet
if "total_consts" is set, report cex's as quasi-genuine
2011-02-28, by blanchet
document new "total_consts" option
2011-02-28, by blanchet
added "total_consts" option
2011-02-28, by blanchet
added a few lemmas by Andreas Lochbihler
2011-02-26, by nipkow
Corrected HOLCF/FOCUS dependency
2011-02-26, by nipkow
Added material by David Trachtenherz
2011-02-26, by nipkow
corrected HOLCF dependency on Nat_Infinity
2011-02-26, by nipkow
got rid of lemma upper_bound_finite_set
2011-02-25, by nipkow
merged
2011-02-25, by nipkow
Some cleaning up
2011-02-25, by nipkow
updated generated files
2011-02-25, by krauss
fixed manual (rule no longer exists)
2011-02-25, by krauss
removed support for tail-recursion from function package (now implemented by partial_function)
2011-02-25, by krauss
reactivate time measurement (partly reverting c27b0b37041a);
2011-02-25, by krauss
generalize find_theorems filters to work on raw propositions, too
2011-02-25, by krauss