isabelle: Graph

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