Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-224
+224
+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.
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
no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
2011-05-03, by blanchet
replaced some Unsynchronized.refs with Config.Ts
2011-05-03, by blanchet
do not declare TPTP built-ins, e.g. $true
2011-05-02, by blanchet
SNARK workaround
2011-05-02, by blanchet
better default type systems for SNARK and ToFoF
2011-05-02, by blanchet
tuning
2011-05-02, by blanchet
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
2011-05-02, by blanchet
generate tags for simps, intros, and elims in TPTP poblems on demand
2011-05-02, by blanchet
proper default for TPTP source filed
2011-05-02, by blanchet
have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-02, by blanchet
eliminated old CVS Ids;
2011-05-02, by wenzelm
no use of package rail;
2011-05-02, by wenzelm
obsolete;
2011-05-02, by wenzelm
removed rail garbage;
2011-05-02, by wenzelm
NEWS;
2011-05-02, by wenzelm
just one railsetup.sty which is shipped with the official distribution to accompany @{rail} in Pure;
2011-05-02, by wenzelm
proper treatment of underscore in rail diagrams;
2011-05-02, by wenzelm
simplified rail setup, using plain defaults (NB: \small is incompatible with \isabellestyle used here);
2011-05-02, by wenzelm
eliminated external rail executable;
2011-05-02, by wenzelm
removed obsolete rail diagrams (which were about old-style theory syntax);
2011-05-02, by wenzelm
moved material about old codegen to isar-ref manual;
2011-05-02, by wenzelm
eliminated some duplicate "def" positions;
2011-05-02, by wenzelm
'axiomatization' is global;
2011-05-02, by wenzelm
discontinued old version of old HOL manual;
2011-05-02, by wenzelm
merged
2011-05-02, by wenzelm
removed obsolete rail setup;
2011-05-02, by wenzelm
uniform content markup;
2011-05-02, by wenzelm
eliminated obsolete rail macros;
2011-05-02, by wenzelm
removed obsolete rail diagram (which was about old-style theory syntax);
2011-05-02, by wenzelm
eliminated separate rail/latex phase;
2011-05-02, by wenzelm
more precise rail diagrams;
2011-05-02, by wenzelm
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
2011-05-02, by wenzelm
make SML/NJ happier
2011-05-02, by blanchet
make "debug" more verbose and "verbose" less verbose
2011-05-02, by blanchet
use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
2011-05-02, by blanchet
cosmetics
2011-05-02, by blanchet
supply type-system defaults for major ATPs
2011-05-02, by blanchet
make sure that "file" annotations are read correctly in SInE-E and E proofs
2011-05-02, by blanchet
fixed random number invocation
2011-05-02, by blanchet
make sure E type information constants are given a weight, even if they don't appear anywhere else
2011-05-02, by blanchet
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
2011-05-02, by blanchet
show sorts not just types in Isar proofs + tuning
2011-05-02, by blanchet
Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly
2011-05-02, by blanchet
tuning
2011-05-02, by blanchet
make SML/NJ happy
2011-05-02, by blanchet
added TPTP exporter facility -- useful to do experiments with machine learning
2011-05-02, by blanchet
renamed theory to make its purpose clearer
2011-05-02, by blanchet
fixing typo
2011-05-02, by bulwahn
improving naming of fresh variables in OCaml serializer
2011-05-02, by bulwahn
adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)
2011-05-02, by bulwahn
merged;
2011-05-02, by wenzelm
modernized rail diagrams using @{rail} antiquotation;
2011-05-02, by wenzelm
tuning
2011-05-02, by blanchet
fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs
2011-05-02, by blanchet
use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...
2011-05-01, by blanchet
beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
2011-05-01, by blanchet
minor doc fixes
2011-05-01, by blanchet
adapt to new type system names
2011-05-01, by blanchet
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01, by blanchet
take "partial_types" option with a grain of salt
2011-05-01, by blanchet
fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
2011-05-01, by blanchet
close formula universally, to make SPASS happy
2011-05-01, by blanchet
fixed embarrassing bug where conjecture and fact offsets were swapped
2011-05-01, by blanchet
pick up GaveUp error on SystemOnTPTP
2011-05-01, by blanchet
avoid trailing digits for SNARK (type) names -- grr...
2011-05-01, by blanchet
document new type system syntax
2011-05-01, by blanchet
use ! for mildly unsound and !! for very unsound encodings
2011-05-01, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip