Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+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.
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
2011-08-15, by wenzelm
explicit check of finished evaluation;
2011-08-15, by wenzelm
refined Document.edit: less stateful update via Graph.schedule;
2011-08-15, by wenzelm
simplified exec: eliminated unused status flag;
2011-08-15, by wenzelm
consistently use variable name 'F' for filters
2011-08-14, by huffman
generalize lemmas about LIM and LIMSEQ to tendsto
2011-08-14, by huffman
HOL-Nominal-Examples: respect distinction between sets and functions
2011-08-13, by huffman
less verbosity in batch mode -- spam reduction and notable performance improvement;
2011-08-13, by wenzelm
merged
2011-08-13, by wenzelm
HOL-Hahn_Banach: use Set_Algebras library
2011-08-13, by huffman
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
2011-08-13, by huffman
clarified Toplevel.end_theory;
2011-08-13, by wenzelm
simplified Toplevel.init_theory: discontinued special name argument;
2011-08-13, by wenzelm
simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13, by wenzelm
provide node header via Scala layer;
2011-08-13, by wenzelm
reduced verbosity;
2011-08-13, by wenzelm
tuned signature;
2011-08-13, by wenzelm
clarified node header -- exclude master_dir;
2011-08-13, by wenzelm
tuned;
2011-08-13, by wenzelm
maintain node header;
2011-08-13, by wenzelm
removed unused lemma; removed old-style ;
2011-08-13, by kleing
point isatest-statistics to the right afp log files
2011-08-13, by kleing
IMP/Util distinguishes between sets and functions again; imported only where used.
2011-08-13, by kleing
remove redundant lemma setsum_norm in favor of norm_setsum;
2011-08-12, by huffman
merged
2011-08-12, by huffman
make more HOL theories work with separate set type
2011-08-12, by huffman
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
2011-08-13, by wenzelm
merged
2011-08-12, by wenzelm
merged
2011-08-12, by huffman
make Multivariate_Analysis work with separate set type
2011-08-12, by huffman
make HOLCF work with separate set type
2011-08-12, by huffman
merged
2011-08-12, by huffman
avoid duplicate rule warnings
2011-08-11, by huffman
modify euclidean_space class to include basis set
2011-08-11, by huffman
remove lemma stupid_ext
2011-08-11, by huffman
documented extended version of case_names attribute
2011-08-12, by nipkow
normalized theory dependencies wrt. file_store;
2011-08-12, by wenzelm
general Graph.schedule;
2011-08-12, by wenzelm
allow "$" within basic path elements (NB: initial "$" refers to path variable);
2011-08-12, by wenzelm
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-12, by wenzelm
simplified class Thy_Header;
2011-08-12, by wenzelm
clarified Exn.message;
2011-08-12, by wenzelm
uniform treatment of header edits as document edits;
2011-08-11, by wenzelm
explicit datatypes for document node edits;
2011-08-11, by wenzelm
tuned;
2011-08-11, by wenzelm
disentangled nested ML files;
2011-08-11, by wenzelm
minimal script to run raw Poly/ML with concurrency library;
2011-08-11, by wenzelm
somewhat more uniform THIS;
2011-08-11, by wenzelm
more trimming;
2011-08-11, by wenzelm
recovered some ML toplevel pp;
2011-08-11, by wenzelm
some trimming;
2011-08-11, by wenzelm
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
2011-08-11, by wenzelm
redundant use of misc_legacy.ML;
2011-08-11, by wenzelm
eliminated use of recdef
2011-08-11, by krauss
removed obsolete recdef-related examples
2011-08-11, by krauss
removed unused material, which does not really belong here
2011-08-11, by krauss
merged
2011-08-10, by huffman
avoid warnings about duplicate rules
2011-08-10, by huffman
follow standard naming scheme for sgn_vec_def
2011-08-10, by huffman
remove several redundant and unused theorems about derivatives
2011-08-10, by huffman
remove redundant lemma
2011-08-10, by huffman
simplify proof of lemma bounded_component
2011-08-10, by huffman
simplify some proofs
2011-08-10, by huffman
more uniform naming scheme for finite cartesian product type and related theorems
2011-08-10, by huffman
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
2011-08-10, by huffman
merged
2011-08-10, by wenzelm
split Linear_Algebra.thy from Euclidean_Space.thy
2011-08-10, by huffman
full import paths
2011-08-10, by huffman
declare tendsto_const [intro] (accidentally removed in 230a8665c919)
2011-08-10, by huffman
merged
2011-08-10, by huffman
simplified definition of class euclidean_space;
2011-08-10, by huffman
bounded_linear interpretation for euclidean_component
2011-08-09, by huffman
lemma bounded_linear_intro
2011-08-09, by huffman
avoid duplicate rewrite warnings
2011-08-09, by huffman
mark some redundant theorems as legacy
2011-08-09, by huffman
Derivative.thy: more sensible subsection headings
2011-08-09, by huffman
Derivative.thy: clean up formatting
2011-08-09, by huffman
instance real_basis_with_inner < perfect_space
2011-08-08, by huffman
old term operations are legacy;
2011-08-10, by wenzelm
moved old code generator to src/Tools/;
2011-08-10, by wenzelm
avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10, by wenzelm
avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10, by wenzelm
avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10, by wenzelm
avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10, by wenzelm
tuned signature;
2011-08-10, by wenzelm
Goal.forked: clarified handling of interrupts;
2011-08-10, by wenzelm
future_job: explicit indication of interrupts;
2011-08-10, by wenzelm
more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
2011-08-10, by wenzelm
synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;
2011-08-10, by wenzelm
tuned source structure;
2011-08-10, by wenzelm
bash_output_fifo blocks on Cygwin 1.7.x;
2011-08-10, by wenzelm
rename_bvs now avoids introducing name clashes between schematic variables
2011-08-09, by berghofe
merged
2011-08-09, by wenzelm
tuned proofs
2011-08-09, by haftmann
merged
2011-08-09, by haftmann
tuned header
2011-08-09, by haftmann
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
2011-08-09, by haftmann
removed "extremely ambigous" warning; has been ignored by everyone for years.
2011-08-09, by kleing
misc tuning and clarification;
2011-08-09, by wenzelm
tuned whitespace;
2011-08-09, by wenzelm
support local HOATPs
2011-08-09, by blanchet
document local HOATPs
2011-08-09, by blanchet
workaround THF parser limitation
2011-08-09, by blanchet
LEO-II also supports FOF
2011-08-09, by blanchet
misc tuning and simplification;
2011-08-09, by wenzelm
updated documentation of method "split" according to e6a4bb832b46;
2011-08-09, by wenzelm
updated references to CADE-23
2011-08-09, by blanchet
renamed E wrappers for consistency with CASC conventions
2011-08-09, by blanchet
updated Sledgehammer docs
2011-08-09, by blanchet
add line number prefix to output file name
2011-08-09, by blanchet
added "sound" option to Mirabelle
2011-08-09, by blanchet
move lambda-lifting code to ATP encoding, so it can be used by Metis
2011-08-09, by blanchet
load lambda-lifting structure earlier, so it can be used in Metis
2011-08-09, by blanchet
merged
2011-08-09, by haftmann
move legacy candiates to bottom; marked candidates for default simp rules
2011-08-08, by haftmann
merged
2011-08-08, by haftmann
dropped lemmas (Inf|Sup)_(singleton|binary)
2011-08-08, by haftmann
dropped lemmas (Inf|Sup)_(singleton|binary)
2011-08-08, by haftmann
rename type 'a net to 'a filter, following standard mathematical terminology
2011-08-08, by huffman
HOLCF: fix warnings about unreferenced identifiers
2011-08-08, by huffman
remove duplicate lemmas
2011-08-08, by huffman
merged
2011-08-08, by huffman
fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39)
2011-08-08, by huffman
generalize sequence lemmas
2011-08-08, by huffman
generalize more lemmas about compactness
2011-08-08, by huffman
generalize compactness equivalence lemmas
2011-08-08, by huffman
lemma bolzano_weierstrass_imp_compact
2011-08-08, by huffman
class perfect_space inherits from topological_space;
2011-08-08, by huffman
merged
2011-08-08, by wenzelm
import constant folding theory into IMP
2011-08-08, by kleing
make syntax ambiguity warnings a config option
2011-08-06, by kleing
add lemmas INF_image, SUP_image
2011-08-08, by huffman
declare {INF,SUP}_empty [simp]
2011-08-08, by huffman
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
2011-08-08, by huffman
standard theorem naming scheme: complex_eqI, complex_eq_iff
2011-08-08, by huffman
moved division ring stuff from Rings.thy to Fields.thy
2011-08-08, by huffman
Library/Product_ord: wellorder instance for products
2011-08-08, by huffman
modernized file proof_checker.ML;
2011-08-08, by wenzelm
tuned thm_of_proof: build lookup table within closure;
2011-08-08, by wenzelm
added Reconstruct.proof_of convenience;
2011-08-08, by wenzelm
ship message in one piece;
2011-08-08, by wenzelm
misc tuning -- eliminated old-fashioned rep_thm;
2011-08-08, by wenzelm
modernized strcture Proof_Checker;
2011-08-08, by wenzelm
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
2011-08-08, by wenzelm
updated imports;
2011-08-08, by wenzelm
proper signature;
2011-08-08, by wenzelm
made SML/NJ happy;
2011-08-08, by wenzelm
slightly more uniform messages;
2011-08-08, by wenzelm
avoid pointless completion of illegal control commands;
2011-08-08, by wenzelm
removed old expand_fun_eq
2011-08-08, by nipkow
fixed index entry
2011-08-08, by nipkow
removed old recdef and types usage
2011-08-08, by nipkow
merged
2011-08-08, by nipkow
extended user-level attribute case_names with names for case hypotheses
2011-08-06, by nipkow
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-08-01, by nipkow
workaround for Java 1.7 where javax.swing.JComboBox<E> is generic;
2011-08-07, by wenzelm
updated version information;
2011-08-07, by wenzelm
fixed document;
2011-08-07, by wenzelm
tuned order: pushing INF and SUP to Inf and Sup
2011-08-05, by haftmann
tuned order: pushing INF and SUP to Inf and Sup
2011-08-05, by haftmann
generalized lemmas to complete lattices
2011-08-05, by haftmann
merged
2011-08-05, by Andreas Lochbihler
replace old SML code generator by new code generator in MicroJava/J
2011-08-05, by Andreas Lochbihler
new state syntax with less conflicts
2011-08-04, by kleing
replace old SML code generator by new code generator in MicroJava/JVM and /BV
2011-08-05, by Andreas Lochbihler
merged
2011-08-05, by haftmann
more fine-granular instantiation
2011-08-04, by haftmann
solving duality problem for complete_distrib_lattice; tuned
2011-08-04, by haftmann
merged
2011-08-04, by berghofe
Pending FDL types may now be associated with Isabelle types as well.
2011-08-04, by berghofe
tuned orthography
2011-08-04, by haftmann
avoid yet unknown fact antiquotation
2011-08-04, by haftmann
NEWS
2011-08-04, by haftmann
more specific instantiation
2011-08-03, by haftmann
tuned
2011-08-03, by haftmann
class complete_distrib_lattice
2011-08-03, by haftmann
NEWS
2011-08-03, by bulwahn
removing value invocations with the SML code generator
2011-08-03, by bulwahn
removing the SML evaluator
2011-08-03, by bulwahn
fixed wrong isubs in IMP/Types
2011-08-03, by kleing
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
2011-08-02, by huffman
NEWS: fix typo
2011-08-02, by huffman
updated unchecked forward reference
2011-08-02, by krauss
replaced Nitpick's hardwired basic_ersatz_table by context data
2011-08-02, by krauss
NEWS
2011-08-02, by krauss
moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
2011-08-02, by krauss
moved recdef package to HOL/Library/Old_Recdef.thy
2011-08-02, by krauss
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
clarified YXML.embed_controls -- this is idempotent and cannot be nested;
2011-07-12, by wenzelm
allow empty body for raw_message -- important for Invoke_Scala;
2011-07-12, by wenzelm
Isabelle string syntax allows literal control characters;
2011-07-12, by wenzelm
glyphs from DejaVu for ASCII control characters 5, 6, 7, 127, which have a special meaning in Isabelle or Poly/ML;
2011-07-12, by wenzelm
more precise exceptions;
2011-07-12, by wenzelm
tuned XML modules;
2011-07-12, by wenzelm
Quotient example: Lists with distinct elements
2011-07-12, by Cezary Kaliszyk
merged
2011-07-11, by wenzelm
explicit code equation for equality
2011-07-11, by haftmann
tuned error messages;
2011-07-11, by wenzelm
tuned;
2011-07-11, by wenzelm
tuned signature -- corresponding to Scala version;
2011-07-11, by wenzelm
made SML/NJ happy;
2011-07-11, by wenzelm
more uniform padded_markup, which is important for caret visibility despite absence of markup;
2011-07-11, by wenzelm
merged
2011-07-11, by wenzelm
merged
2011-07-11, by haftmann
tuned proofs
2011-07-10, by haftmann
tuned notation
2011-07-10, by haftmann
tuned notation
2011-07-10, by haftmann
tuned notation
2011-07-10, by haftmann
NEWS;
2011-07-11, by wenzelm
proper InvocationTargetException.getCause for indirect exceptions;
2011-07-11, by wenzelm
tuned error message;
2011-07-11, by wenzelm
tuned signature;
2011-07-11, by wenzelm
JVM method invocation service via Scala layer;
2011-07-11, by wenzelm
tuned signature;
2011-07-11, by wenzelm
some support for raw messages, which bypass standard Symbol/YXML decoding;
2011-07-11, by wenzelm
tuned XML.Cache parameters;
2011-07-11, by wenzelm
some support to invoke Scala methods under program control;
2011-07-10, by wenzelm
merged;
2011-07-10, by wenzelm
merged
2011-07-10, by haftmann
tuned proofs and notation
2011-07-10, by haftmann
more succinct proofs
2011-07-10, by haftmann
more succinct proofs
2011-07-10, by haftmann
adding a very liberal timeout for values after a test case failed due to the restricted timeout
2011-07-10, by bulwahn
improved NEWS
2011-07-10, by bulwahn
NEWS
2011-07-09, by bulwahn
standardized String.concat towards implode (cf. c37a1f29bbc0)
2011-07-09, by bulwahn
adding quickcheck examples for evaluating floor and ceiling functions
2011-07-09, by bulwahn
adding code equations to execute floor and ceiling on rational and real numbers
2011-07-09, by bulwahn
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
2011-07-09, by bulwahn
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
2011-07-10, by wenzelm
lambda terms with XML data representation in Scala;
2011-07-10, by wenzelm
XML data representation of lambda terms;
2011-07-10, by wenzelm
YXML.string_of_body convenience;
2011-07-10, by wenzelm
made SML/NJ happy;
2011-07-10, by wenzelm
tuned signature;
2011-07-10, by wenzelm
more abstract signature;
2011-07-10, by wenzelm
simplified XML_Data;
2011-07-10, by wenzelm
less currying in Scala;
2011-07-10, by wenzelm
propagate header changes to prover process;
2011-07-10, by wenzelm
echo prover input via raw_messages, for improved protocol tracing;
2011-07-09, by wenzelm
tuned;
2011-07-09, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip