Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
document new type system and soundness properties of the different systems
2011-05-20, by blanchet
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
2011-05-20, by blanchet
reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
2011-05-20, by blanchet
more doc fiddling
2011-05-20, by blanchet
more FAQs
2011-05-20, by blanchet
make sure the Vampire incomplete proof detection code kicks in
2011-05-20, by blanchet
automatically use "metisFT" when typed helpers are necessary
2011-05-20, by blanchet
tuning
2011-05-20, by blanchet
generate useful information for type axioms
2011-05-20, by blanchet
slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
2011-05-20, by blanchet
updated FAQ
2011-05-20, by blanchet
more informative message when Sledgehammer finds an unsound proof
2011-05-20, by blanchet
tuned proofs
2011-05-20, by haftmann
NEWS
2011-05-20, by haftmann
point-free characterization of operations on finite sets
2011-05-20, by haftmann
merged
2011-05-20, by haftmann
names of fold_set locales resemble name of characteristic property more closely
2011-05-20, by haftmann
clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton
2011-05-20, by krauss
use point-free characterization for locale fun_left_comm_idem
2011-05-20, by haftmann
tuned proof
2011-05-20, by haftmann
Collect intro-rules for sigma-algebras
2011-05-17, by hoelzl
the measurable sets with null measure form a ring
2011-05-17, by hoelzl
add some lemmas for infinite product measure
2011-05-17, by hoelzl
add measurable_Least
2011-05-17, by hoelzl
add restrict_sigma
2011-05-17, by hoelzl
add borel_eq_atLeastLessThan
2011-05-17, by hoelzl
Add formalization of probabilistic independence for families of sets
2011-05-17, by hoelzl
add Bernoulli space
2011-05-19, by hoelzl
add product of probability spaces with finite cardinality
2011-05-19, by hoelzl
remove double sum_over_space_real_distribution
2011-05-19, by hoelzl
a deeper understanding of the code generation adaptation compared to 9079f49053e5
2011-05-19, by bulwahn
updated option documentation
2011-05-19, by blanchet
renamed "simple_types" to "simple"
2011-05-19, by blanchet
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
2011-05-19, by blanchet
tweaked ATP type systems further based on Judgment Day
2011-05-19, by blanchet
honor "conj_sym_kind" also for tag symbol declarations
2011-05-19, by blanchet
removed "poly_tags_light_bang" since highly unsound
2011-05-19, by blanchet
distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
2011-05-19, by blanchet
reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
2011-05-19, by blanchet
fixed empty proof detection
2011-05-19, by blanchet
tuning
2011-05-19, by blanchet
minor doc fixes
2011-05-19, by blanchet
mention version 0.6 of Vampire, since that's what's currently available for download
2011-05-19, by blanchet
better error reporting: detect missing E proofs and remove Vampire native format error
2011-05-19, by blanchet
NEWS
2011-05-18, by bulwahn
adding Code_Char_ord to code generation regression tests
2011-05-18, by bulwahn
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
2011-05-18, by bulwahn
removed some obsolete text;
2011-05-20, by wenzelm
basic support for overpainting of text, imitating jEdit internals;
2011-05-18, by wenzelm
some support for token/chunk handling, imitating jEdit internals;
2011-05-17, by wenzelm
renamed thin to light, fat to heavy
2011-05-17, by blanchet
code cleanup, better handling of corner cases
2011-05-17, by blanchet
run blacklist algorithm only if slicing is on
2011-05-17, by blanchet
implemented thin versions of "preds" type systems + fixed various issues with type args
2011-05-17, by blanchet
use antiquotation
2011-05-17, by blanchet
renamed "shallow" to "thin" and make it the default
2011-05-17, by blanchet
more work on "shallow" encoding + adjustments to other encodings
2011-05-17, by blanchet
generate type classes predicates in new "shallow" encoding
2011-05-17, by blanchet
started implementing "shallow" type systems, based on ideas by Claessen et al.
2011-05-17, by blanchet
added syntax for "shallow" encodings
2011-05-17, by blanchet
provide isabellep as a method
2011-05-17, by blanchet
append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
2011-05-17, by blanchet
tuned;
2011-05-16, by wenzelm
less fine-grained mira dependencies
2011-05-16, by krauss
mira hack for special settings on lxbroy10
2011-05-16, by krauss
no dependencies for Isabelle_makeall, which will be built in one go
2011-05-16, by krauss
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
2011-05-16, by krauss
future merge of grammars, to improve parallel performance;
2011-05-15, by wenzelm
only show relevant timing;
2011-05-15, by wenzelm
timing of Theory_Data operations, with implicit thread positions when functor is applied;
2011-05-15, by wenzelm
tuned;
2011-05-15, by wenzelm
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
2011-05-15, by wenzelm
NEWS (cf. 4e8483cc2cc5);
2011-05-15, by wenzelm
simplified/unified method_setup/attribute_setup;
2011-05-15, by wenzelm
optional description for 'attribute_setup' and 'method_setup';
2011-05-15, by wenzelm
tuned signature;
2011-05-15, by wenzelm
merged
2011-05-14, by wenzelm
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
2011-05-14, by wenzelm
use pointfree characterisation for fold_set locale
2011-05-14, by haftmann
discontinued global config options within attribute name space;
2011-05-14, by wenzelm
more precise warnings: observe context visibility;
2011-05-14, by wenzelm
modernized structure Rule_Insts;
2011-05-14, by wenzelm
discontinued old / unused addss' (cf. 57f364d1d3b2);
2011-05-14, by wenzelm
eliminated global Unsynchronized.ref;
2011-05-14, by wenzelm
proper runtime context for auto_inv_tac;
2011-05-14, by wenzelm
simplified BLAST_DATA;
2011-05-14, by wenzelm
proper Proof.context -- eliminated global operations;
2011-05-14, by wenzelm
just one universal Proof.context -- discontinued claset/clasimpset;
2011-05-14, by wenzelm
modernized functor names;
2011-05-14, by wenzelm
method "deepen" with optional limit;
2011-05-14, by wenzelm
merged
2011-05-13, by wenzelm
removed redundant type annotations and duplicate examples
2011-05-13, by krauss
clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-13, by wenzelm
make ZF_cs snapshot after final setup;
2011-05-13, by wenzelm
proper Proof.context for classical tactics;
2011-05-13, by wenzelm
do not open ML structures;
2011-05-13, by wenzelm
eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
2011-05-13, by wenzelm
misc tuning and simplification;
2011-05-13, by wenzelm
tuned proof;
2011-05-13, by wenzelm
tuned proof;
2011-05-13, by wenzelm
proper method_setup;
2011-05-13, by wenzelm
proper method_setup "split_idle";
2011-05-13, by wenzelm
proper method_setup "enabled";
2011-05-13, by wenzelm
simplified clasimpset declarations -- prefer attributes;
2011-05-13, by wenzelm
reduce the number of mono iterations to prevent the mono code from going berserk
2011-05-13, by blanchet
tuned comment
2011-05-13, by blanchet
optimized a common case
2011-05-13, by blanchet
avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed
2011-05-13, by blanchet
tweak E slices
2011-05-13, by blanchet
make SML/NJ happy
2011-05-13, by blanchet
fixed off-by-one bug
2011-05-13, by blanchet
added convenience syntax
2011-05-13, by blanchet
prefer Proof.context over old-style claset/simpset;
2011-05-12, by wenzelm
prefer plain simpset operations;
2011-05-12, by wenzelm
removed obsolete old-style cs/css;
2011-05-12, by wenzelm
modernized dead code;
2011-05-12, by wenzelm
eliminated old-style MI_fast_css -- replaced by fast_solver with config option;
2011-05-12, by wenzelm
eliminated obsolete MI_css -- use current context directly;
2011-05-12, by wenzelm
proper method_setup;
2011-05-12, by wenzelm
modernized simproc_setup;
2011-05-12, by wenzelm
prefer Proof.context over old-style clasimpset;
2011-05-12, by wenzelm
modernized dead code;
2011-05-12, by wenzelm
modernized specifications;
2011-05-12, by wenzelm
merged
2011-05-12, by wenzelm
added hints and FAQs
2011-05-12, by blanchet
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
2011-05-12, by blanchet
fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
2011-05-12, by blanchet
another concession to backward compatibility
2011-05-12, by blanchet
no need to use metisFT for Isar proofs -- metis falls back on it anyway
2011-05-12, by blanchet
handle equality proxy in a more backward-compatible way
2011-05-12, by blanchet
remove problematic Isar proof
2011-05-12, by blanchet
added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
2011-05-12, by blanchet
robustly detect how many type args were passed to the ATP, even if some of them were omitted
2011-05-12, by blanchet
make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
2011-05-12, by blanchet
drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
2011-05-12, by blanchet
tuning
2011-05-12, by blanchet
fixed conjecture resolution bug for Vampire 1.0's TSTP output
2011-05-12, by blanchet
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
2011-05-12, by blanchet
Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it
2011-05-12, by blanchet
drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines
2011-05-12, by blanchet
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
2011-05-12, by blanchet
further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
2011-05-12, by blanchet
reenabled equality proxy in Metis for higher-order reasoning
2011-05-12, by blanchet
added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file
2011-05-12, by blanchet
reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions
2011-05-12, by blanchet
unfold set constants in Sledgehammer/ATP as well if Metis does it too
2011-05-12, by blanchet
do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
2011-05-12, by blanchet
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12, by blanchet
added unfold set constant functionality to Meson/Metis -- disabled by default for now
2011-05-12, by blanchet
remove unused parameter
2011-05-12, by blanchet
reduced penalty associated with existential quantifiers
2011-05-12, by blanchet
ensure that Auto Sledgehammer is run with full type information
2011-05-12, by blanchet
fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
2011-05-12, by blanchet
don't give weights to built-in symbols
2011-05-12, by blanchet
more robust exception handling in Metis (also works if there are several subgoals)
2011-05-12, by blanchet
no penality for constants that appear in chained facts
2011-05-12, by blanchet
gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers
2011-05-12, by blanchet
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
2011-05-12, by blanchet
tune whitespace
2011-05-12, by blanchet
added configuration options for experimental features
2011-05-12, by blanchet
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
2011-05-12, by blanchet
avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense
2011-05-12, by blanchet
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
2011-05-12, by blanchet
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-12, by blanchet
allow each slice to have its own type system
2011-05-12, by blanchet
renamed type systems for more consistency
2011-05-12, by blanchet
updated versions;
2011-05-12, by wenzelm
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
2011-05-12, by wenzelm
tuned;
2011-05-12, by wenzelm
minor adaption for scala-2.9.0.final;
2011-05-12, by wenzelm
proper configuration options Proof_Context.debug and Proof_Context.verbose;
2011-05-12, by wenzelm
pretend that all versions of BSD are Linux, which might actually work due to binary compatibilty mode of these obsolete platforms;
2011-05-12, by wenzelm
more uniform naming of lemma
2011-05-12, by haftmann
add a lemma about commutative append to List.thy
2011-05-09, by noschinl
removed assumption from lemma List.take_add
2011-05-09, by noschinl
no need for underscore.sty -- latex.ltx provides \textunderscore and \_ already;
2011-05-06, by wenzelm
removed \underscoreon which is from Larry's iman.sty, not underscore.sty;
2011-05-06, by wenzelm
further improved type system setup based on Judgment Days
2011-05-06, by blanchet
allow each prover to specify its own formula kind for symbols occurring in the conjecture
2011-05-06, by blanchet
better type system setup, based on Judgment Day
2011-05-06, by blanchet
improving merge of code specifications by removing code equations of constructors after merging two theories
2011-05-06, by bulwahn
tuned;
2011-05-05, by wenzelm
tuned some syntax names;
2011-05-05, by wenzelm
tuned rail diagrams and layout;
2011-05-05, by wenzelm
merged;
2011-05-05, by wenzelm
tuning
2011-05-05, by blanchet
reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
2011-05-05, by blanchet
added FIXME
2011-05-05, by blanchet
no lies in debug output (e.g. "slice 2 of 1")
2011-05-05, by blanchet
help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
2011-05-05, by blanchet
query typedefs as well for monotonicity
2011-05-05, by blanchet
adding examples for invoking quickcheck with records
2011-05-05, by bulwahn
adding creation of exhaustive generators for records; simplifying dependencies in Main theory
2011-05-05, by bulwahn
hopefully this will help the SML/NJ type inference
2011-05-05, by blanchet
reverted 6efda6167e5d because unsound -- Vampire found a counterexample
2011-05-05, by blanchet
improve suggested type system list based on evaluation
2011-05-05, by blanchet
I have an intuition that it's sound to omit the first type arg of an hAPP -- and this reduces the size of monomorphized problems quite a bit
2011-05-05, by blanchet
removed unsound hAPP optimization
2011-05-05, by blanchet
versions of ! and ? for the ASCII-challenged Mirabelle
2011-05-05, by blanchet
smoother handling of ! and ? in type system names
2011-05-05, by blanchet
tuning
2011-05-04, by blanchet
compile + added monotonicity tests
2011-05-04, by blanchet
documentation tuning
2011-05-04, by blanchet
renamed "many_typed" to "simple" (as in simple types)
2011-05-04, by blanchet
update type system documentation
2011-05-04, by blanchet
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
2011-05-04, by blanchet
document monotonic type systems
2011-05-04, by blanchet
exploit inferred monotonicity
2011-05-04, by blanchet
[mq]: nitpick_tuning
2011-05-04, by blanchet
fixed cardinality computation for function types such as "'a -> unit"
2011-05-04, by blanchet
monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
2011-05-04, by blanchet
proper case_names for int_cases, int_of_nat_induct;
2011-05-04, by wenzelm
added type annotation for SML/NJ
2011-05-04, by blanchet
eta-expansion for SML/NJ
2011-05-04, by blanchet
removed odd historical material;
2011-05-03, by wenzelm
merged
2011-05-03, by wenzelm
fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
2011-05-03, by blanchet
cosmetics
2011-05-03, by blanchet
more conventional naming scheme: names_long, names_short, names_unique;
2011-05-03, by wenzelm
railsetup required for IsarRef/style;
2011-05-03, by wenzelm
fit page;
2011-05-03, by wenzelm
use existing \<hyphen>;
2011-05-03, by wenzelm
more precise syntax diagram;
2011-05-03, by wenzelm
simplified rail configuration;
2011-05-03, by wenzelm
provide \isabellestyle{itunderscore} (requires underscore.sty);
2011-05-03, by wenzelm
updated generated files;
2011-05-03, by wenzelm
proper treatment of empty name -- avoid excessive vertical space;
2011-05-03, by wenzelm
final \makeatother -- catcodes appear to be global;
2011-05-03, by wenzelm
fixed long name truncation logic
2011-05-03, by blanchet
some documentation of @{rail} antiquotation;
2011-05-03, by wenzelm
more precise source position for @{rail};
2011-05-03, by wenzelm
sane paragraph layout;
2011-05-03, by wenzelm
updated configuration options -- no ML here;
2011-05-03, by wenzelm
tag ML as in IsarImplementation;
2011-05-03, by wenzelm
treat underscore as in IsarRef;
2011-05-03, by wenzelm
reactivated codegen example based on Lambda.thy;
2011-05-03, by wenzelm
formal Base theory;
2011-05-03, by wenzelm
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
2011-05-03, by blanchet
whitespace tuning
2011-05-03, by blanchet
make SML/NJ happiest
2011-05-03, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip