isabelle: Graph

prefer functional modes of functions in the mode analysis
2010-04-21, by bulwahn
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-04-21, by bulwahn
merged
2010-04-21, by hoelzl
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
2010-04-21, by hoelzl
Translated remaining theorems about integration from HOL light.
2010-04-20, by himmelma
marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);
2010-04-21, by wenzelm
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
2010-04-20, by huffman
Remove garbage.
2010-04-20, by ballarin
Remove garbage.
2010-04-20, by ballarin
recovered isabelle java, which was broken in ebfa4bb0d50f;
2010-04-20, by wenzelm
fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared;
2010-04-20, by blanchet
merged
2010-04-20, by blanchet
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
2010-04-20, by blanchet
merge
2010-04-20, by blanchet
cosmetics
2010-04-19, by blanchet
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
2010-04-19, by blanchet
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
2010-04-19, by blanchet
added warning about inconsistent context to Metis;
2010-04-19, by blanchet
workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted
2010-04-19, by blanchet
got rid of somewhat pointless "pairname" function in Sledgehammer
2010-04-19, by blanchet
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
cosmetics
2010-04-19, by blanchet
make Sledgehammer's minimizer also minimize Isar proofs
2010-04-19, by blanchet
don't use readable names if proof reconstruction is needed, because it uses the structure of names
2010-04-19, by blanchet
allow "_" in TPTP names in debug mode
2010-04-19, by blanchet
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-19, by blanchet
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
2010-04-19, by blanchet
get rid of "List.foldl" + add timestamp to SPASS
2010-04-19, by blanchet
less ambitious settings for cygwin-poly;
2010-04-20, by wenzelm
respectfullness and preservation of map for identity quotients
2010-04-20, by Cezary Kaliszyk
respectfullness and preservation of function composition
2010-04-20, by Cezary Kaliszyk
eta-normalize the goal since the original theorem is atomized
2010-04-20, by Cezary Kaliszyk
accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;
2010-04-20, by wenzelm
refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;
2010-04-20, by wenzelm
merged
2010-04-20, by haftmann
more appropriate representation of valid positions for abstractors
2010-04-19, by haftmann
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
2010-04-19, by haftmann
update_syntax: add new productions only once, to allow repeated local notation, for example;
2010-04-19, by wenzelm
tuned;
2010-04-19, by wenzelm
more platform information;
2010-04-19, by wenzelm
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
2010-04-19, by wenzelm
some updates on multi-platform support;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
explicit check sorts in abstract certificates; abstractor is part of dependencies
2010-04-19, by haftmann
polyml-platform script is superseded by ISABELLE_PLATFORM;
2010-04-19, by wenzelm
less ambitious settings for cygwin-poly;
2010-04-19, by wenzelm
merged
2010-04-19, by haftmann
more convenient equations for zip
2010-04-19, by haftmann
more platform info;
2010-04-17, by wenzelm
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
2010-04-17, by wenzelm
system properties determine the JVM platform, not the Isabelle one;
2010-04-17, by wenzelm
THIS_CYGWIN;
2010-04-17, by wenzelm
improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
2010-04-17, by wenzelm
isatest: more robust treatment of remote files, less reliance on mounted file system;
2010-04-17, by wenzelm
merged
2010-04-17, by blanchet
added missing \n in output
2010-04-17, by blanchet
by default, don't try to start ATPs that aren't installed
2010-04-16, by blanchet
fiddle with Sledgehammer option syntax
2010-04-16, by blanchet
added timestamp to proof
2010-04-16, by blanchet
restore order of clauses in TPTP output;
2010-04-16, by blanchet
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
2010-04-16, by blanchet
output total time taken by Sledgehammer if "verbose" is set
2010-04-16, by blanchet
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
2010-04-16, by blanchet
reorganize Sledgehammer's relevance filter slightly
2010-04-16, by blanchet
tell the user that Sledgehammer kills its siblings
2010-04-16, by blanchet
updated keywords;
2010-04-16, by wenzelm
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
2010-04-16, by wenzelm
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16, by wenzelm
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
2010-04-16, by wenzelm
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16, by wenzelm
allow syntax types within abbreviations;
2010-04-16, by wenzelm
modernized old-style type abbreviations;
2010-04-16, by wenzelm
modernized type abbreviations;
2010-04-16, by wenzelm
local type abbreviations;
2010-04-16, by wenzelm
merged
2010-04-16, by blanchet
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16, by blanchet
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-16, by blanchet
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-04-15, by blanchet
make Sledgehammer's output more debugging friendly
2010-04-15, by blanchet
made SML/NJ happy;
2010-04-16, by wenzelm
proper masking of dummy name_space;
2010-04-16, by wenzelm
salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;
2010-04-16, by wenzelm
proper checking of ML functors (in Poly/ML 5.2 or later);
2010-04-16, by wenzelm
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
2010-04-16, by wenzelm
isatest: improved treatment of local files on atbroy102;
2010-04-16, by wenzelm
add rule deflation_ID to proof script for take + constructor rules
2010-04-15, by huffman
more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);
2010-04-15, by wenzelm
HOL record: explicitly allow sort constraints;
2010-04-15, by wenzelm
misc tuning and simplification;
2010-04-15, by wenzelm
explicit ProofContext.check_tfree;
2010-04-15, by wenzelm
merged
2010-04-15, by wenzelm
Respectfullness and preservation of list_rel
2010-04-15, by Cezary Kaliszyk
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
2010-04-15, by wenzelm
get_sort: suppress dummyS from input;
2010-04-15, by wenzelm
modernized treatment of sort constraints in specification;
2010-04-15, by wenzelm
typecopy: observe given sort constraints more precisely;
2010-04-15, by wenzelm
inline old Record.read_typ/cert_typ;
2010-04-15, by wenzelm
spelling;
2010-04-15, by wenzelm
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
2010-04-15, by haftmann
tuned whitespace;
2010-04-14, by wenzelm
merged
2010-04-14, by wenzelm
merged
2010-04-14, by blanchet
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
2010-04-14, by blanchet
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-04-14, by blanchet
make Sledgehammer's "timeout" option work for "minimize"
2010-04-14, by blanchet
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
2010-04-14, by blanchet
Spelling error: theroems -> theorems
2010-04-14, by hoelzl
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
2010-04-14, by krauss
record package: corrected sort handling in type translations to avoid crashes when default sort is changed.
2010-04-14, by krauss
more precise treatment of UNC server prefix, e.g. //foo;
2010-04-14, by wenzelm
support named_root, which approximates UNC server prefix (for Cygwin);
2010-04-14, by wenzelm
updated Thm.add_axiom/add_def;
2010-04-14, by wenzelm
adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;
2010-04-14, by wenzelm
bring HOLCF/ex/Domain_Proofs.thy up to date
2010-04-13, by huffman
adapt Refute example to reflect latest soundness fix to Refute
2010-04-13, by blanchet
commented out unsound "lfp"/"gfp" handling + fixed set output syntax;
2010-04-13, by blanchet
merged
2010-04-13, by blanchet
make Nitpick output everything to tracing in debug mode;
2010-04-13, by blanchet
fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")
2010-04-13, by blanchet
cosmetics
2010-04-13, by blanchet
merge
2010-04-13, by Cezary Kaliszyk
merge
2010-04-13, by Cezary Kaliszyk
add If respectfullness and preservation to Quotient package database
2010-04-13, by Cezary Kaliszyk
more accurate pattern match
2010-04-13, by haftmann
dropped dead code
2010-04-13, by haftmann
update domain package examples
2010-04-12, by huffman
remove dead code
2010-04-12, by huffman
share more code between definitional and axiomatic domain packages
2010-04-12, by huffman
for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML
2010-04-12, by huffman
Changed the type of Quot_True, so that it is an HOL constant.
2010-04-12, by Cezary Kaliszyk
removed rather toyish tree
2010-04-11, by haftmann
updated keywords
2010-04-11, by haftmann
merged
2010-04-11, by haftmann
user interface for abstract datatypes is an attribute, not a command
2010-04-11, by haftmann
implementation of mappings by rbts
2010-04-11, by haftmann
lemma is_empty_empty
2010-04-11, by haftmann
constructor Mapping replaces AList
2010-04-11, by haftmann
stay within Local_Defs layer;
2010-04-11, by wenzelm
expose foundational typedef axiom name;
2010-04-11, by wenzelm
Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-04-11, by wenzelm
modernized datatype constructors;
2010-04-11, by wenzelm
of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;
2010-04-11, by wenzelm
tuned;
2010-04-11, by wenzelm
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
2010-04-11, by wenzelm
include JEDIT_APPLE_PROPERTIES by default;
2010-04-09, by wenzelm
isatest: more uniform setup for Unix vs. Cygwin;
2010-04-09, by wenzelm
added missing case: meta universal quantifier
2010-04-08, by boehmes
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
2010-04-08, by bulwahn
Merged.
2010-04-07, by ballarin
Merged resolving conflicts NEWS and locale.ML.
2010-04-07, by ballarin
Proper inheritance of mixins for activated facts and locale dependencies.
2010-04-02, by ballarin
Removed obsolete function.
2010-02-15, by ballarin
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
2010-02-15, by ballarin
Tuned interpretation proofs.
2010-02-15, by ballarin
A rough implementation of full mixin inheritance; additional unit tests.
2010-02-11, by ballarin
Clarified invariant; tuned.
2010-02-02, by ballarin
More mixin tests.
2010-02-01, by ballarin
Use serial to be more debug friendly.
2010-02-01, by ballarin
buffered output (faster than direct output)
2010-04-07, by boehmes
simplified Cache_IO interface (input is just a string and not already stored in a file)
2010-04-07, by boehmes
shortened interface (do not export unused options and functions)
2010-04-07, by boehmes
always unfold definitions of specific constants (including special binders)
2010-04-07, by boehmes
shorten the code by conditional function application
2010-04-07, by boehmes
fail for problems containg the universal sort (as those problems cannot be atomized)
2010-04-07, by boehmes
renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
2010-04-07, by boehmes
Added Information theory and Example: dining cryptographers
2010-04-07, by hoelzl
simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
2010-04-07, by Christian Urban
removed (latex output) notation which is sometimes very ugly
2010-04-06, by krauss
merged
2010-04-06, by boehmes
added missing mult_1_left to linarith simp rules
2010-04-06, by boehmes
tuned proof (no induction needed); removed unused lemma and fuzzy comment
2010-04-06, by krauss
isatest: basic setup for cygwin-poly on atbroy102;
2010-04-02, by wenzelm
slightly more standard dependencies;
2010-04-01, by wenzelm
merged
2010-04-01, by nipkow
tuned many proofs a bit
2010-04-01, by nipkow
merged
2010-04-01, by nipkow
documented [[trace_simp=true]]
2010-03-29, by nipkow
add missing goal argument
2010-04-01, by blanchet
adapt syntax of Sledgehammer options in examples
2010-04-01, by blanchet
merged
2010-04-01, by blanchet
fixed layout of Sledgehammer output
2010-04-01, by blanchet
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
2010-03-29, by blanchet
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
2010-03-29, by blanchet
get rid of Polyhash, since it's no longer used
2010-03-29, by blanchet
remove use of Polyhash;
2010-03-29, by blanchet
reintroduce efficient set structure to collect "no_atp" theorems
2010-03-29, by blanchet
made "theory_const" a Sledgehammer option;
2010-03-29, by blanchet
added "respect_no_atp" and "convergence" options to Sledgehammer;
2010-03-29, by blanchet
adding MREC induction rule in Imperative HOL
2010-03-31, by bulwahn
made smlnj happy
2010-03-31, by bulwahn
adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned
2010-03-31, by bulwahn
adopting specialisation examples to moving the alternative defs in the library
2010-03-31, by bulwahn
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
2010-03-31, by bulwahn
no specialisation for predicates without introduction rules in the predicate compiler
2010-03-31, by bulwahn
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
2010-03-31, by bulwahn
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes
2010-03-31, by bulwahn
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
2010-03-31, by bulwahn
clarifying the Predicate_Compile_Core signature
2010-03-31, by bulwahn
adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure
2010-03-31, by bulwahn
putting compilation setup of predicate compiler in a separate file
2010-03-31, by bulwahn
simplify fold_graph proofs
2010-03-30, by huffman
NEWS
2010-03-30, by krauss
removed dead code; fixed typo
2010-03-30, by krauss
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
2010-03-30, by krauss
merged
2010-03-30, by wenzelm
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
2010-03-29, by bulwahn
tuned
2010-03-29, by bulwahn
generalized alternative functions to alternative compilation to handle arithmetic functions better
2010-03-29, by bulwahn
correcting alternative functions with tuples
2010-03-29, by bulwahn
no specialisation for patterns with only tuples in the predicate compiler
2010-03-29, by bulwahn
adding registration of functions in the function flattening
2010-03-29, by bulwahn
added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
2010-03-29, by bulwahn
adding specialisation examples of the predicate compiler
2010-03-29, by bulwahn
adding specialisation of predicates to the predicate compiler
2010-03-29, by bulwahn
returning an more understandable user error message in the values command
2010-03-29, by bulwahn
adding Lazy_Sequences with explicit depth-bound
2010-03-29, by bulwahn
removing fishing for split thm in the predicate compiler
2010-03-29, by bulwahn
prefer recursive calls before others in the mode inference
2010-03-29, by bulwahn
added statistics to values command for random generation
2010-03-29, by bulwahn
adopting Predicate_Compile_Quickcheck
2010-03-29, by bulwahn
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
2010-03-29, by bulwahn
removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
2010-03-29, by bulwahn
adding a hook for experiments in the predicate compilation process
2010-03-29, by bulwahn
removing simple equalities in introduction rules in the predicate compiler
2010-03-29, by bulwahn
adopting Predicate_Compile
2010-03-29, by bulwahn
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
2010-03-29, by bulwahn
generalizing the compilation process of the predicate compiler
2010-03-29, by bulwahn
added new compilation to predicate_compiler
2010-03-29, by bulwahn
adding new depth-limited and new random monad for the predicate compiler
2010-03-29, by bulwahn
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
2010-03-30, by wenzelm
adapted to Scala 2.8.0 Beta 1;
2010-03-30, by wenzelm
auto update by Netbeans 6.8;
2010-03-30, by wenzelm
adapted to Netbeans 6.8 and Scala for Netbeans 6.8v1.1;
2010-03-30, by wenzelm
replaced some deprecated methods;
2010-03-29, by wenzelm
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
2010-03-29, by wenzelm
merged
2010-03-29, by huffman
use lattice theorems to prove set theorems
2010-03-28, by huffman
add/change some lemmas about lattices
2010-03-28, by huffman