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.
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
2010-09-17, by wenzelm
Isabelle_Markup.overview_color: indicate error / warning messages;
2010-09-17, by wenzelm
some specific message classification;
2010-09-17, by wenzelm
Syntax.read_asts error: report token ranges within message -- no side-effect here;
2010-09-17, by wenzelm
Isabelle_Process: status/report do not require serial numbers;
2010-09-17, by wenzelm
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip