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
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.
simplified some internal flags using Config.T instead of full-blown Proof_Data;
2010-09-17, by wenzelm
tuned signature of (Context_)Position.report variants;
2010-09-17, by wenzelm
merged
2010-09-17, by wenzelm
merged
2010-09-17, by blanchet
update README
2010-09-17, by blanchet
regenerate "metis.ML"
2010-09-17, by blanchet
fix license
2010-09-17, by blanchet
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
2010-09-17, by blanchet
move functions around
2010-09-17, by blanchet
simplify Skolem handling;
2010-09-17, by blanchet
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
2010-09-17, by blanchet
complete refactoring of Metis along the lines of Sledgehammer
2010-09-16, by blanchet
got caught once again by SML's pattern maching (ctor vs. var)
2010-09-16, by blanchet
added new "Metis_Reconstruct" module, temporarily empty
2010-09-16, by blanchet
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
2010-09-16, by blanchet
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
2010-09-16, by blanchet
skip some "important" messages
2010-09-16, by blanchet
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
2010-09-16, by blanchet
merged
2010-09-17, by nipkow
added lemmas
2010-09-17, by nipkow
merged
2010-09-17, by haftmann
proper closures for static evaluation; no need for FIXMEs any longer
2010-09-17, by haftmann
refined static_eval_conv_simple; tuned comments
2010-09-17, by haftmann
closures preserve static serializer context for static evaluation; tuned
2010-09-17, by haftmann
closures separate serializer initialization from serializer invocation as far as appropriate
2010-09-17, by haftmann
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
2010-09-17, by boehmes
made sml/nj happy
2010-09-17, by haftmann
merged
2010-09-16, by haftmann
added code_stmts antiquotation from doc-src/more_antiquote.ML
2010-09-16, by haftmann
added output_typewriter from doc-src/more_antiquote.ML
2010-09-16, by haftmann
moved material intro distribution proper
2010-09-16, by haftmann
merged
2010-09-16, by haftmann
merged
2010-09-16, by haftmann
separation of static and dynamic thy context
2010-09-16, by haftmann
adjusted setup
2010-09-16, by haftmann
dynamic and static value computation; built-in evaluation of propositions
2010-09-16, by haftmann
Exn.map_result
2010-09-16, by haftmann
adjusted to changes in Code_Runtime
2010-09-16, by haftmann
merged
2010-09-16, by bulwahn
merged
2010-09-16, by bulwahn
improving replacing higher order arguments to work with tuples
2010-09-16, by bulwahn
adding another context free grammar example for the predicate compiler
2010-09-16, by bulwahn
adding values to show and ensure that values works with complex terms and restores numerals on natural numbers
2010-09-16, by bulwahn
adding restoring of numerals for natural numbers for values command
2010-09-16, by bulwahn
values command for prolog supports complex terms and not just variables
2010-09-16, by bulwahn
adapting examples
2010-09-16, by bulwahn
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
2010-09-16, by bulwahn
adding mode inference to prolog compilation; separate between (ad-hoc) code modifications and system_configuration; adapting quickcheck
2010-09-16, by bulwahn
merged
2010-09-16, by paulson
tidied a few proofs
2010-09-16, by paulson
merged
2010-09-16, by blanchet
avoid code duplication
2010-09-16, by blanchet
tuning
2010-09-16, by blanchet
merge constructors
2010-09-16, by blanchet
factor out the inverse of "nice_atp_problem"
2010-09-16, by blanchet
use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
2010-09-16, by blanchet
factored out TSTP/SPASS/Vampire proof parsing;
2010-09-16, by blanchet
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
2010-09-16, by blanchet
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
2010-09-16, by blanchet
regenerated "metis.ML"
2010-09-16, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip