Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+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.
added dynamic ersatz_table to Nitpick's data slot
2011-08-02, by krauss
eliminated obsolete recdef/wfrec related declarations
2011-08-02, by krauss
more consistent naming in IMP/Comp_Rev
2011-08-01, by kleing
merged
2011-08-01, by haftmann
tuned proofs
2011-07-30, by haftmann
tuned proofs
2011-07-29, by haftmann
new theory HOL/Library/Product_Lattice.thy
2011-08-01, by huffman
domain package: more informative error message for illegal indirect recursion
2011-07-31, by huffman
compiler proof cleanup
2011-07-28, by kleing
added helpers for "All" and "Ex"
2011-07-28, by blanchet
put parentheses around non-trivial metis call
2011-07-28, by blanchet
no needless mangling
2011-07-28, by blanchet
resolved code_pred FIXME in IMP; clearer notation for exec_n
2011-07-28, by kleing
clean up temporary directory hack
2011-07-28, by blanchet
tuning
2011-07-28, by blanchet
fixed lambda concealing
2011-07-28, by blanchet
make SML/NJ happy
2011-07-28, by blanchet
simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)
2011-07-28, by hoelzl
document coercions
2011-07-28, by noschinl
rudimentary documentation of the quotient package in the isar reference manual
2011-07-27, by bulwahn
to_nat is injective on arbitrary domains
2011-07-27, by hoelzl
finite vimage on arbitrary domains
2011-07-27, by hoelzl
updated Sledgehammer documentation
2011-07-26, by blanchet
renamed "preds" encodings to "guards"
2011-07-26, by blanchet
more precise dependencies
2011-07-26, by bulwahn
further worked around LEO-II parser limitation, with eta-expansion
2011-07-26, by blanchet
use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
2011-07-26, by blanchet
no need for existential witnesses for sorts in TFF and THF formats
2011-07-26, by blanchet
mangle "undefined"
2011-07-26, by blanchet
tuning -- remove useless function (at this point combinators are already in)
2011-07-26, by blanchet
remove spurious message
2011-07-26, by blanchet
give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
2011-07-26, by blanchet
merged
2011-07-26, by Andreas Lochbihler
fixed code generator setup in List_Cset
2011-07-26, by Andreas Lochbihler
enat is a complete_linorder instance
2011-07-26, by hoelzl
merged
2011-07-26, by Andreas Lochbihler
Add theory for setting up monad syntax for Cset
2011-07-26, by Andreas Lochbihler
merged
2011-07-26, by bulwahn
removing expectations from quickcheck example
2011-07-26, by bulwahn
adding remarks after static inspection of the invocation of the SML code generator
2011-07-26, by bulwahn
merged
2011-07-26, by Andreas Lochbihler
added operations to Cset with code equations in backing implementations
2011-07-25, by Andreas Lochbihler
merged
2011-07-25, by haftmann
adjusted to tailored version of ball_simps
2011-07-25, by haftmann
adjusted to tailored version of bex_simps
2011-07-24, by haftmann
more coherent structure in and across theories
2011-07-24, by haftmann
declare "undefined" constant
2011-07-25, by blanchet
make compile
2011-07-25, by blanchet
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
2011-07-25, by blanchet
tuning
2011-07-25, by blanchet
introduced hybrid lambda translation
2011-07-25, by blanchet
avoid needless type args for lifted-lambdas
2011-07-25, by blanchet
replacing conversion function of old code generator by the current code generator in the reflection tactic
2011-07-25, by bulwahn
fixed typo
2011-07-25, by bulwahn
removing SML_Quickcheck
2011-07-25, by bulwahn
NEWS
2011-07-25, by bulwahn
added legacy warning to old code generation evaluation
2011-07-25, by bulwahn
added legacy warning to old code generation commands
2011-07-25, by bulwahn
merged
2011-07-23, by wenzelm
correcting last example in Predicate_Compile_Examples
2011-07-23, by bulwahn
make double-sure that interrupts are flushed before executing new work (cf. 22f8c2483bd2);
2011-07-23, by wenzelm
more detailed tracing;
2011-07-23, by wenzelm
defensive Term_Sharing, to avoid extending trusted code base of inference kernel;
2011-07-23, by wenzelm
more precise parse_name according to XML standard;
2011-07-23, by wenzelm
explicit structure ML_System;
2011-07-23, by wenzelm
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-23, by wenzelm
tuned;
2011-07-23, by wenzelm
merged
2011-07-22, by haftmann
dropped errorneous hint
2011-07-22, by haftmann
moved some lemmas
2011-07-21, by haftmann
merged
2011-07-21, by haftmann
ereal is a complete_linorder instance
2011-07-21, by haftmann
class complete_linorder
2011-07-20, by haftmann
make "concealed" lambda translation sound
2011-07-21, by blanchet
deactivating all quickcheck invocations until parallel invocation works safely
2011-07-21, by bulwahn
adapting two examples in Predicate_Compile_Examples
2011-07-21, by bulwahn
use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
2011-07-20, by blanchet
merge
2011-07-20, by Cezary Kaliszyk
Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
2011-07-20, by Cezary Kaliszyk
add code generator setup and tests for ereal
2011-07-20, by hoelzl
removed debugging facilities accidentally left in the committed code
2011-07-20, by boehmes
more precise dependencies
2011-07-20, by boehmes
merged
2011-07-20, by boehmes
generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
2011-07-20, by boehmes
moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
2011-07-20, by boehmes
removed old (unused) SMT monomorphizer
2011-07-20, by boehmes
added UNION
2011-07-20, by krauss
merged
2011-07-20, by hoelzl
rename Fin to enat
2011-07-19, by hoelzl
add ereal to typeclass infinity
2011-07-19, by hoelzl
add nat => enat coercion
2011-07-19, by hoelzl
Introduce infinity type class
2011-07-19, by hoelzl
Rename extreal => ereal
2011-07-19, by hoelzl
rename Nat_Infinity (inat) to Extended_Nat (enat)
2011-07-19, by hoelzl
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
2011-07-20, by Cezary Kaliszyk
build an image for HOL-IMP
2011-07-20, by kleing
deactivating quickcheck invocation in this example until the Interrupt issue is understood
2011-07-20, by bulwahn
removing inner time limits in quickcheck
2011-07-20, by bulwahn
updating documentation about quickcheck; adding information about try
2011-07-20, by bulwahn
adapting example in Predicate_Compile_Examples
2011-07-20, by bulwahn
exporting function in quickcheck; adapting mutabelle script
2011-07-20, by bulwahn
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
2011-07-20, by bulwahn
making messages more informative
2011-07-20, by bulwahn
only use exhaustive testing in this quickcheck example
2011-07-20, by bulwahn
parse equalities correctly in Nitrox parser
2011-07-20, by blanchet
pass type arguments to lambda-lifted Frees, to account for polymorphism
2011-07-20, by blanchet
generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
2011-07-20, by blanchet
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
2011-07-20, by blanchet
remove offset from Mirabelle output
2011-07-20, by blanchet
the HOL4PROOFS setting is actually HOL4_PROOFS
2011-07-19, by krauss
merged
2011-07-19, by haftmann
proof tuning
2011-07-18, by haftmann
generalization; various notation and proof tuning
2011-07-18, by haftmann
avoid misunderstandable names
2011-07-18, by haftmann
moved lemmas to appropriate theory
2011-07-18, by haftmann
forgotten qualifier
2011-07-19, by krauss
values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
2011-07-19, by krauss
killed use of PolyML.makestring
2011-07-18, by krauss
added experimental mira configuration for HOL Light importer
2011-07-18, by krauss
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
2011-07-18, by boehmes
unactivating narrowing-based quickcheck by default
2011-07-18, by bulwahn
making active configuration public in narrowing-based quickcheck
2011-07-18, by bulwahn
declare tester in this quickcheck example
2011-07-18, by bulwahn
adding code equations for partial_term_of for rational numbers
2011-07-18, by bulwahn
adapting an experimental setup to changes in quickcheck's infrastructure
2011-07-18, by bulwahn
adding narrowing instances for real and rational
2011-07-18, by bulwahn
adapting quickcheck based on the analysis of the predicate compiler
2011-07-18, by bulwahn
adapting prolog-based tester
2011-07-18, by bulwahn
quickcheck does not deactivate testers if none are given
2011-07-18, by bulwahn
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
2011-07-18, by bulwahn
renaming quickcheck_tester to quickcheck_batch_tester; tuned
2011-07-18, by bulwahn
changing parser in quickcheck to activate and deactivate the testers
2011-07-18, by bulwahn
adapting SML_Quickcheck to new quickcheck infrastructure
2011-07-18, by bulwahn
enabling parallel execution of testers but removing more informative quickcheck output
2011-07-18, by bulwahn
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
2011-07-18, by bulwahn
removing generator registration
2011-07-18, by bulwahn
parametrized test_term functions in quickcheck
2011-07-18, by bulwahn
adding random, exhaustive and SML quickcheck as testers
2011-07-18, by bulwahn
more on complement
2011-07-17, by haftmann
more on complement
2011-07-17, by haftmann
more consistent theorem names
2011-07-17, by haftmann
more lemmas about SUP
2011-07-17, by haftmann
structuring duals together
2011-07-17, by haftmann
merged
2011-07-17, by haftmann
more lemmas about Sup
2011-07-17, by haftmann
generalized INT_anti_mono
2011-07-17, by haftmann
moving UNIV = ... equations to their proper theories
2011-07-17, by haftmann
further generalization from sets to complete lattices
2011-07-17, by haftmann
fixed lambda-liftg: must ensure the formulas are in close form
2011-07-17, by blanchet
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
2011-07-17, by blanchet
pass kind to lambda-translation function
2011-07-17, by blanchet
more refactoring of preprocessing
2011-07-17, by blanchet
more refactoring of preprocessing, so as to be able to centralize it
2011-07-17, by blanchet
renamed internal data structure
2011-07-17, by blanchet
simplify code -- there are no lambdas in helpers anyway
2011-07-17, by blanchet
added lambda-lifting to Sledgehammer (rough)
2011-07-17, by blanchet
move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
2011-07-17, by blanchet
merged
2011-07-17, by haftmann
generalized some lemmas
2011-07-16, by haftmann
consolidated bot and top classes, tuned notation
2011-07-16, by haftmann
tuned notation
2011-07-16, by haftmann
clarified bash_output_fifo;
2011-07-16, by wenzelm
moved bash operations to Isabelle_System (cf. Scala version);
2011-07-16, by wenzelm
access to process output stream via auxiliary fifo;
2011-07-16, by wenzelm
some file and directory operations;
2011-07-16, by wenzelm
more general bash_process, which allows to terminate background processes as well;
2011-07-16, by wenzelm
updated to Poly/ML SVN 1328, which is considered 5.4.2;
2011-07-16, by wenzelm
added File.fold_pages for streaming of large files;
2011-07-16, by wenzelm
tuned;
2011-07-16, by wenzelm
HOL/Import: Fix errors with _mk_list
2011-07-16, by Cezary Kaliszyk
Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
2011-07-15, by wenzelm
simplified malformed YXML markup -- special controls are visible in IsabelleText font;
2011-07-15, by wenzelm
less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp;
2011-07-15, by wenzelm
more robust Binding.pretty/print in typical error sitations with spaces etc. (NB: markup can only provide *additional* emphasis and is occasionally suppressed in TTY mode or tooltips);
2011-07-15, by wenzelm
more visible printing of empty binding;
2011-07-15, by wenzelm
do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;
2011-07-15, by wenzelm
more quotes;
2011-07-14, by wenzelm
merged
2011-07-14, by wenzelm
added missing dependencies;
2011-07-14, by krauss
merged
2011-07-14, by haftmann
merged
2011-07-14, by haftmann
tuned notation and proofs
2011-07-14, by haftmann
move error logic closer to user
2011-07-14, by blanchet
allow lambda-lifting without triggers
2011-07-14, by blanchet
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
2011-07-14, by blanchet
added option to control which lambda translation to use (for experiments)
2011-07-14, by blanchet
fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem
2011-07-14, by blanchet
use monomorphic encoding as fallback, since they tend to produce fewer type errors
2011-07-14, by blanchet
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
2011-07-14, by blanchet
clearer unsound message
2011-07-14, by blanchet
clarify fine soundness point
2011-07-14, by blanchet
always unfold "Let"s is Sledgehammer, Metis, and MESON
2011-07-14, by blanchet
unbreak Nitrox's parsing
2011-07-14, by blanchet
merged
2011-07-14, by haftmann
tuned lemma positions and proofs
2011-07-14, by haftmann
tuned notation
2011-07-14, by haftmann
uniqueness lemmas for bot and top
2011-07-13, by haftmann
adjusted to tightened specification of classes bot and top
2011-07-13, by haftmann
moved lemmas bot_less and less_top to classes bot and top respectively
2011-07-13, by haftmann
tightened specification of classes bot and top: uniqueness of top and bot elements
2011-07-13, by haftmann
honor the TPTP environment variable as the root of include relative paths -- that's a weird convention but without it Nitrox will fail at CASC
2011-07-13, by blanchet
better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6
2011-07-13, by blanchet
more exhaustive testing in Nitrox
2011-07-13, by blanchet
no timeout for Nitrox
2011-07-13, by blanchet
avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
2011-07-13, by blanchet
added arithmetic decision procedure to CASC setup
2011-07-13, by blanchet
added some arithmetic functions, for THF with arithmetic
2011-07-13, by blanchet
pull in arithmetic theories
2011-07-13, by blanchet
cleanly separate TPTP related files from other examples
2011-07-13, by blanchet
increasing timeout to avoid spurious failures
2011-07-13, by bulwahn
merged
2011-07-13, by haftmann
more generalization towards complete lattices
2011-07-13, by haftmann
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
2011-07-13, by krauss
merge
2011-07-13, by Cezary Kaliszyk
Tuned
2011-07-13, by Cezary Kaliszyk
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
2011-07-14, by wenzelm
added term_sharing.ML;
2011-07-13, by wenzelm
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
2011-07-13, by wenzelm
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
2011-07-13, by wenzelm
low-level tuning;
2011-07-13, by wenzelm
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
2011-07-13, by wenzelm
XML.pretty with depth limit;
2011-07-13, by wenzelm
more thorough Variable.check_name: Binding.check for logical entities within the term language;
2011-07-12, by wenzelm
tuned;
2011-07-12, by wenzelm
merged
2011-07-12, by wenzelm
Update HOLLightCompat
2011-07-13, by Cezary Kaliszyk
Update files generated in HOL/Import/HOLLight
2011-07-13, by Cezary Kaliszyk
HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
2011-07-13, by Cezary Kaliszyk
ML pp for XML.tree;
2011-07-12, by wenzelm
made SML/NJ happy;
2011-07-12, by wenzelm
clarified YXML.detect;
2011-07-12, by wenzelm
retain some terminology of "XML attributes";
2011-07-12, by wenzelm
more uniform Properties in ML and Scala;
2011-07-12, by wenzelm
more uniform Term and Term_XML modules;
2011-07-12, by wenzelm
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
2011-07-12, by wenzelm
tuned signature -- less cryptic ASCII names;
2011-07-12, by wenzelm
discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;
2011-07-12, by wenzelm
added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
2011-07-12, by wenzelm
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
2011-07-12, by wenzelm
more precise Symbol_Pos.quote_string;
2011-07-12, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip