isabelle: Graph

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