isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle