Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-1920
+1920
+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.
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
2011-11-04, by wenzelm
document new experimental provers
2011-11-04, by blanchet
added remote iProver(-Eq) for experimentation
2011-11-04, by blanchet
merged
2011-11-04, by wenzelm
ex/Tree23.thy: automate proof of gfull_add
2011-11-04, by huffman
ex/Tree23.thy: simplify proof of bal_del0
2011-11-04, by huffman
ex/Tree23.thy: simplify proof of bal_add0
2011-11-04, by huffman
ex/Tree23.thy: simpler definition of ordered-ness predicate
2011-11-04, by huffman
ex/Tree23.thy: prove that deletion preserves balance
2011-11-03, by huffman
more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);
2011-11-04, by wenzelm
more general Proof_Context.bind_propp, which allows outer parameters;
2011-11-03, by wenzelm
tuned whitespace;
2011-11-03, by wenzelm
tuned signature;
2011-11-03, by wenzelm
tuned signature -- canonical argument order;
2011-11-03, by wenzelm
tuned -- Variable.declare_term is already part of Variable.auto_fixes;
2011-11-03, by wenzelm
ex/Tree23.thy: prove that insertion preserves tree balance and order
2011-11-03, by huffman
more IMP fragments
2011-11-03, by kleing
string -> vname
2011-11-03, by kleing
JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
2011-11-03, by kleing
more IMP text fragments
2011-11-03, by kleing
moved latex generation for HOL-IMP out of distribution
2011-11-03, by kleing
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
2011-11-01, by bulwahn
merged
2011-10-31, by bulwahn
more robust, declarative and unsurprising computation of types in the quotient type definition
2011-10-31, by bulwahn
improve handling of bound type variables (esp. for TFF1)
2011-10-31, by blanchet
improved TFF1 output
2011-10-31, by blanchet
clarified signature
2011-10-31, by bulwahn
tuned
2011-10-31, by bulwahn
tuned
2011-10-31, by bulwahn
even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);
2011-10-30, by wenzelm
removed obsolete argument (cf. aa35859c8741);
2011-10-30, by wenzelm
removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]
2011-10-30, by huffman
extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
2011-10-30, by huffman
merged
2011-10-30, by huffman
remove unused function
2011-10-29, by huffman
also export DFG formats
2011-10-29, by blanchet
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
2011-10-29, by blanchet
added DFG unsorted support (like in the old days)
2011-10-29, by blanchet
gracefully do nothing if the SPASS input file is already in DFG format
2011-10-29, by blanchet
added sorted DFG output for coming version of SPASS
2011-10-29, by blanchet
specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9
2011-10-29, by blanchet
check "sound" flag before doing something unsound...
2011-10-29, by blanchet
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
2011-10-29, by wenzelm
tuned;
2011-10-29, by wenzelm
more accurate class constraints on cancellation simproc patterns
2011-10-28, by huffman
tuned;
2011-10-29, by wenzelm
tuned Named_Thms: proper binding;
2011-10-28, by wenzelm
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
2011-10-28, by wenzelm
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
2011-10-28, by wenzelm
uniform Local_Theory.declaration with explicit params;
2011-10-28, by wenzelm
tuned signature -- refined terminology;
2011-10-28, by wenzelm
slightly more explicit/syntactic modelling of morphisms;
2011-10-28, by wenzelm
correct import path
2011-10-28, by hoelzl
allow to build Probability and MV-Analysis with one ROOT.ML
2011-10-28, by hoelzl
removing dead code
2011-10-28, by bulwahn
ex/Simproc_Tests.thy: remove duplicate simprocs
2011-10-28, by huffman
use simproc_setup for cancellation simprocs, to get proper name bindings
2011-10-28, by huffman
tuned;
2011-10-27, by wenzelm
eliminated aliases of standard functions;
2011-10-27, by wenzelm
more standard attribute setup;
2011-10-27, by wenzelm
localized quotient data;
2011-10-27, by wenzelm
simplified/standardized signatures;
2011-10-27, by wenzelm
tuned signature;
2011-10-27, by wenzelm
uses IMP and hence requires its tex setup
2011-10-27, by nipkow
merged
2011-10-27, by nipkow
tuned text
2011-10-27, by nipkow
respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception
2011-10-27, by bulwahn
respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
2011-10-27, by bulwahn
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
2011-10-27, by bulwahn
merged
2011-10-27, by huffman
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-10-27, by huffman
more robust ML pretty printing (cf. b6c527c64789);
2011-10-26, by wenzelm
tuned;
2011-10-26, by wenzelm
renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library
2011-10-25, by bulwahn
tuned text
2011-10-25, by nipkow
tuned names to avoid shadowing
2011-10-25, by nipkow
merge Gcd/GCD and Lcm/LCM
2011-10-25, by huffman
clarify types of terms: use proper set type
2011-10-25, by boehmes
instance bool :: linorder
2011-10-24, by huffman
removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
2011-10-24, by bulwahn
fixed typo
2011-10-24, by bulwahn
latex output not needed because errors manifest themselves earlier
2011-10-24, by nipkow
some text on inner-syntax;
2011-10-23, by wenzelm
renamed in ASM
2011-10-23, by nipkow
tuned order of eqns
2011-10-23, by nipkow
tuned
2011-10-23, by nipkow
script for exporting filtered IMP files as tar.gz
2011-10-23, by kleing
removed Norbert's email from isatest (bounces)
2011-10-23, by kleing
class Lexicon as abstract datatype;
2011-10-22, by wenzelm
more private stuff;
2011-10-22, by wenzelm
class Text.Edit as abstract datatype;
2011-10-22, by wenzelm
class Time as abstract datatype;
2011-10-22, by wenzelm
class Volatile as abstract datatype;
2011-10-22, by wenzelm
merged
2011-10-22, by nipkow
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
2011-10-22, by nipkow
experimental support for Scala 2.9.1.final;
2011-10-22, by wenzelm
class Path as abstract datatype;
2011-10-22, by wenzelm
class Counter as abstract datatype;
2011-10-22, by wenzelm
discontinued redundant ASCII syntax;
2011-10-22, by wenzelm
modernized specifications;
2011-10-22, by wenzelm
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
2011-10-21, by wenzelm
merged
2011-10-21, by nipkow
tuned
2011-10-21, by nipkow
merged
2011-10-21, by wenzelm
replacing metis proofs with facts xt1 by new proof with more readable names
2011-10-21, by bulwahn
more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
2011-10-21, by blanchet
disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction
2011-10-21, by blanchet
NEWS
2011-10-21, by bulwahn
updating documentation: code_inline -> code_unfold; added documentation about attribute code_unfold_post
2011-10-21, by bulwahn
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-10-21, by bulwahn
removing redundant attribute code_inline in the code generator
2011-10-21, by bulwahn
tuned;
2011-10-21, by wenzelm
tuned;
2011-10-21, by wenzelm
improving mutabelle script again after missing some changes in f4896c792316
2011-10-21, by bulwahn
correcting code_prolog
2011-10-21, by bulwahn
merged
2011-10-21, by huffman
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
2011-10-21, by huffman
merged
2011-10-21, by nipkow
tuned
2011-10-21, by nipkow
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
2011-10-20, by blanchet
merged
2011-10-20, by huffman
removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
2011-10-20, by huffman
removed [trans] concept from basic material
2011-10-20, by kleing
merged
2011-10-20, by nipkow
tuned
2011-10-20, by nipkow
merged
2011-10-20, by bulwahn
modernizing predicate_compile_quickcheck
2011-10-20, by bulwahn
adding depth as an quickcheck configuration
2011-10-20, by bulwahn
renamed name -> vname
2011-10-20, by nipkow
removed some remaining artefacts of ancient SML code generator
2011-10-19, by haftmann
NEWS
2011-10-19, by haftmann
cleaner LEO-II extensionality step detection
2011-10-19, by blanchet
marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
2011-10-19, by blanchet
one more LEO-II failure
2011-10-19, by blanchet
merged
2011-10-19, by wenzelm
merged
2011-10-19, by huffman
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
2011-10-18, by huffman
more uniform SZS status handling
2011-10-19, by blanchet
avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"
2011-10-19, by blanchet
merged
2011-10-19, by nipkow
renamed B to Bc
2011-10-19, by nipkow
tuned comment;
2011-10-19, by wenzelm
proper source positions for @{lemma};
2011-10-19, by wenzelm
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
2011-10-19, by wenzelm
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
2011-10-19, by wenzelm
tuned legacy signature;
2011-10-19, by wenzelm
further cleanup of stats (cf. 97e81a8aa277);
2011-10-19, by wenzelm
updated keywords;
2011-10-19, by wenzelm
really document just one code generator;
2011-10-19, by wenzelm
NEWS
2011-10-19, by bulwahn
removing old code generator
2011-10-19, by bulwahn
removing declaration of code_unfold to address the old code generator
2011-10-19, by bulwahn
removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const
2011-10-19, by bulwahn
removing documentation about the old code generator
2011-10-19, by bulwahn
removing old code generator setup for executable sets
2011-10-19, by bulwahn
removing old code generator setup for efficient natural numbers; cleaned typo
2011-10-19, by bulwahn
removing old code generator setup for real numbers; tuned
2011-10-19, by bulwahn
removing old code generator setup for rational numbers; tuned
2011-10-19, by bulwahn
removing old code generator setup for strings
2011-10-19, by bulwahn
removing old code generator setup for lists
2011-10-19, by bulwahn
removing old code generator setup for integers
2011-10-19, by bulwahn
removing old code generator for inductive predicates
2011-10-19, by bulwahn
removing quickcheck tester SML-inductive based on the old code generator
2011-10-19, by bulwahn
removing old code generator setup for inductive sets in the inductive set package
2011-10-19, by bulwahn
removing old code generator setup of inductive predicates
2011-10-19, by bulwahn
removing old code generator setup for product types
2011-10-19, by bulwahn
removing old code generator setup for function types
2011-10-19, by bulwahn
removing old code generator setup for datatypes
2011-10-19, by bulwahn
removing old code generator for recursive functions
2011-10-19, by bulwahn
removing old code generator setup in the HOL theory
2011-10-19, by bulwahn
removing invocations of the evaluation method based on the old code generator
2011-10-19, by bulwahn
removing invocations of the old code generator
2011-10-19, by bulwahn
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
2011-10-18, by blanchet
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
2011-10-18, by blanchet
tuned
2011-10-18, by bulwahn
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
2011-10-18, by bulwahn
mira: collect size of heap images
2011-10-18, by krauss
updated doc related to Satallax
2011-10-17, by blanchet
parse Satallax unsat cores
2011-10-17, by blanchet
merged
2011-10-17, by wenzelm
(old) NEWS
2011-10-17, by noschinl
moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
2011-10-17, by bulwahn
always use sockets on Windows/Cygwin;
2011-10-17, by wenzelm
mira configuration: use official polyml 5.4.1 on lxbroy10
2011-10-16, by krauss
added Term.dummy_pattern conveniences;
2011-10-16, by wenzelm
slightly more standard-conformant XML parsing (see also 94033767ef9b);
2011-10-16, by wenzelm
tuned proof
2011-10-16, by haftmann
tuned type annnotation
2011-10-16, by haftmann
hide not_member as also member
2011-10-16, by haftmann
misc tuning and modernization;
2011-10-15, by wenzelm
updated to Scala 2.8.2.final;
2011-10-15, by wenzelm
prefer recent polyml-5.4.1, but retain potentially fragile polyml-5.2.1 as experimental test;
2011-10-15, by wenzelm
updated to polyml-5.4.1;
2011-10-15, by wenzelm
updated to polyml-5.4.1;
2011-10-15, by wenzelm
merged
2011-10-15, by haftmann
monadic bind
2011-10-14, by haftmann
moved sublists to More_List.thy
2011-10-14, by haftmann
NEWS
2011-10-14, by haftmann
more complete stats, including small sessions which provide some clues on main HOL baseline performance;
2011-10-14, by wenzelm
avoid very specific code equation for card; corrected spelling
2011-10-13, by haftmann
bouned transitive closure
2011-10-13, by haftmann
moved acyclic predicate up in hierarchy
2011-10-13, by haftmann
tuned
2011-10-13, by haftmann
modernized definitions
2011-10-13, by haftmann
static dummy_task (again) to avoid a few extra allocations;
2011-10-13, by wenzelm
tuned markup
2011-10-13, by noschinl
discontinued obsolete 'types' command;
2011-10-13, by wenzelm
modernized structure Induct_Tacs;
2011-10-12, by wenzelm
tuned signature;
2011-10-12, by wenzelm
misc tuning and clarification;
2011-10-12, by wenzelm
tuned ML style;
2011-10-12, by wenzelm
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-10-12, by wenzelm
discontinued obsolete alias structure ProofContext;
2011-10-12, by wenzelm
separated monotonicity reasoning and defined narrowing with while_option
2011-10-12, by nipkow
include no-smlnj targets into library (cf. e54a985daa61);
2011-10-10, by wenzelm
increasing values_timeout to avoid SML_makeall failures on our current tests
2011-10-10, by bulwahn
merged
2011-10-10, by wenzelm
removed obsolete RC tags;
2011-10-10, by wenzelm
Int.thy: discontinued some legacy theorems
2011-10-09, by huffman
Set.thy: remove redundant [simp] declarations
2011-10-09, by huffman
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
2011-10-03, by bulwahn
tune text for document generation
2011-10-03, by bulwahn
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
2011-10-03, by bulwahn
adding code equations for cardinality and (reflexive) transitive closure on finite types
2011-10-03, by bulwahn
adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
2011-10-03, by bulwahn
adding lemma to List library for executable equation of the (refl) transitive closure
2011-10-03, by bulwahn
fixed typos in IMP
2011-09-29, by Jean Pichon
added nice interval syntax
2011-09-28, by nipkow
Added dependecies
2011-09-28, by nipkow
Added Hoare-like Abstract Interpretation
2011-09-28, by nipkow
moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
2011-09-28, by nipkow
back to post-release mode;
2011-09-26, by wenzelm
Added tag Isabelle2011-1 for changeset 76fef3e57004
2011-10-09, by wenzelm
tuned;
Isabelle2011-1
2011-10-09, by wenzelm
updated ISABELLE_HOME_USER;
2011-10-09, by wenzelm
more explicit check of Java executable -- relevant for Linux x86/x86_64 mismatch and absence on Mac OS Lion;
2011-10-04, by wenzelm
Added tag Isabelle2011-1-RC2 for changeset a45121ffcfcb
2011-10-03, by wenzelm
some amendments due to Jean Pichon;
2011-10-03, by wenzelm
correct coercion generation in case of unknown map functions
2011-09-29, by traytel
proper platform_file_url for Windows UNC paths (server shares);
2011-09-28, by wenzelm
proper platform_file_url;
2011-09-27, by wenzelm
observe base URL of rendered document;
2011-09-27, by wenzelm
more README;
2011-09-27, by wenzelm
tuned README.html;
2011-09-27, by wenzelm
tuned;
2011-09-27, by wenzelm
retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);
2011-09-27, by wenzelm
tuned message, which is displayed after termination of Isabelle.app on Mac OS;
2011-09-27, by wenzelm
keep top-level "Isabelle" executable -- now an alias for "isabelle jedit";
2011-09-26, by wenzelm
tuned;
2011-09-26, by wenzelm
ensure Isabelle env;
2011-09-26, by wenzelm
Added tag Isabelle2011-1-RC1 for changeset 24ad77c3a147
2011-09-26, by wenzelm
tuned;
2011-09-26, by wenzelm
misc tuning for release;
2011-09-26, by wenzelm
reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
2011-09-26, by wenzelm
makedist for release;
2011-09-26, by wenzelm
put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes
2011-09-26, by blanchet
require Java 1.6 in the Nitpick documentation -- technically 1.5 will also work with Kodkodi 1.2.16, but it won't work with Kodkodi 1.5.0
2011-09-26, by blanchet
put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
2011-09-26, by blanchet
adding an example with inductive predicates to quickcheck narrowing examples
2011-09-26, by bulwahn
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
2011-09-26, by bulwahn
clarify platforms
2011-09-25, by blanchet
killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore
2011-09-25, by blanchet
updated Nitpick SAT Solver doc
2011-09-25, by blanchet
update list of SAT solvers reflecting Kodkod 1.5
2011-09-25, by blanchet
tuned signature;
2011-09-25, by wenzelm
more uniform defaults;
2011-09-25, by wenzelm
Quotient_Set.thy is part of library
2011-09-25, by haftmann
fixed typo
2011-09-25, by nipkow
standardize drive letters -- important for proper document node identification;
2011-09-24, by wenzelm
more user aliases;
2011-09-24, by wenzelm
fixed IsaMakefile action for HOL-TPTP.
2011-09-24, by sultana
prefer socket comminication on Cygwin, which is more stable here than fifos;
2011-09-23, by wenzelm
tuned proof;
2011-09-23, by wenzelm
made SML/NJ happy;
2011-09-23, by wenzelm
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
2011-09-23, by wenzelm
updated header;
2011-09-23, by wenzelm
merged;
2011-09-23, by wenzelm
reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
2011-09-23, by blanchet
first step towards extending Minipick with more translations
2011-09-23, by blanchet
Include keywords print_coercions and print_coercion_maps
2011-09-23, by berghofe
local coercion insertion algorithm to support complex coercions
2011-08-17, by traytel
printing and deleting of coercions
2011-08-17, by traytel
raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
2011-09-23, by wenzelm
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
2011-09-23, by wenzelm
augment existing print mode;
2011-09-23, by wenzelm
explicit option for socket vs. fifo communication;
2011-09-23, by wenzelm
tuned proof;
2011-09-23, by wenzelm
synchronized section names with manual
2011-09-23, by blanchet
merged;
2011-09-23, by wenzelm
discontinued legacy theorem names from RealDef.thy
2011-09-22, by huffman
merged
2011-09-22, by huffman
discontinued HOLCF legacy theorem names
2011-09-22, by huffman
take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime
2011-09-22, by blanchet
Moved extraction part of Higman's lemma to separate theory to allow reuse in
2011-09-22, by berghofe
Removed hcentering and vcentering options, since they are not supported
2011-09-22, by berghofe
merged
2011-09-22, by berghofe
Added documentation for HOL-SPARK
2011-09-22, by berghofe
drop partial monomorphic instances in Metis, like in Sledgehammer
2011-09-22, by blanchet
better type reconstruction -- prevents ill-instantiations in proof replay
2011-09-22, by blanchet
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
2011-09-22, by hoelzl
changing quickcheck_timeout to 30 seconds in mutabelle's testing
2011-09-22, by bulwahn
adding post-processing of terms to narrowing-based Quickcheck
2011-09-22, by bulwahn
HOL/ex/ROOT.ML: only list BinEx once
2011-09-21, by huffman
merged
2011-09-21, by huffman
remove redundant instantiation ereal :: power
2011-09-21, by huffman
reintroduced Minipick as Nitpick example
2011-09-21, by blanchet
tuned comment
2011-09-21, by blanchet
merged
2011-09-21, by huffman
Extended_Real_Limits: generalize some lemmas
2011-09-20, by huffman
add lemmas within_empty and tendsto_bot;
2011-09-20, by huffman
made SML/NJ happy;
2011-09-22, by wenzelm
abstract System_Channel in ML (cf. Scala version);
2011-09-22, by wenzelm
alternative Socket_Channel;
2011-09-21, by wenzelm
more abstract wrapping of fifos as System_Channel;
2011-09-21, by wenzelm
slightly more general Socket_IO as part of Pure;
2011-09-21, by wenzelm
more hints on Z3 configuration;
2011-09-21, by wenzelm
reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);
2011-09-21, by wenzelm
renamed inv -> filter
2011-09-21, by nipkow
Added proofs about narowing
2011-09-21, by nipkow
added missing makefile dependence
2011-09-21, by nipkow
added example
2011-09-21, by nipkow
tuned
2011-09-21, by nipkow
refined comment
2011-09-21, by nipkow
fixed two typos in IMP (by Jean Pichon)
2011-09-21, by kleing
merged
2011-09-21, by nipkow
Updated IMP to use new induction method
2011-09-20, by nipkow
New proof method "induction" that gives induction hypotheses the name IH.
2011-09-20, by nipkow
official status for UN_singleton
2011-09-20, by haftmann
tuned specification and lemma distribution among theories; tuned proofs
2011-09-20, by haftmann
more careful treatment of initial update, similar to output panel;
2011-09-20, by wenzelm
proper fact binding;
2011-09-20, by wenzelm
syntactic improvements and tuning names in the code generator due to Florian's code review
2011-09-20, by bulwahn
match types when applying mono_thm -- previous export generalizes type variables;
2011-09-20, by krauss
fixed headers;
2011-09-19, by wenzelm
less ambiguous syntax;
2011-09-19, by wenzelm
tuned proofs;
2011-09-19, by wenzelm
merged
2011-09-19, by wenzelm
catch PatternMatchFail exceptions in narrowing-based quickcheck
2011-09-19, by bulwahn
removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
2011-09-19, by bulwahn
ensuring that some constants are generated in the source code by adding calls in ensure_testable
2011-09-19, by bulwahn
adding abstraction layer; more precise function names
2011-09-19, by bulwahn
adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
2011-09-19, by bulwahn
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
2011-09-19, by bulwahn
only annotating constants with sort constraints
2011-09-19, by bulwahn
also adding type annotations for the dynamic invocation
2011-09-19, by bulwahn
removed legacy lemmas in Complete_Lattices
2011-09-19, by noschinl
increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling
2011-09-19, by bulwahn
more isatest stats;
2011-09-19, by wenzelm
refined Symbol.is_symbolic -- cover recoded versions as well;
2011-09-19, by wenzelm
double clicks switch to document node buffer;
2011-09-19, by wenzelm
tuned;
2011-09-19, by wenzelm
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
2011-09-19, by wenzelm
at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
2011-09-19, by wenzelm
instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);
2011-09-19, by wenzelm
unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
2011-09-19, by wenzelm
imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;
2011-09-19, by wenzelm
merged
2011-09-18, by huffman
numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
2011-09-15, by huffman
removed obsolete patches for PG 4.1;
2011-09-18, by wenzelm
additional space for borderless UI;
2011-09-18, by wenzelm
more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);
2011-09-18, by wenzelm
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
2011-09-18, by wenzelm
isatest settings for macbroy6 (Mac OS X Lion);
2011-09-18, by wenzelm
more Mac OS reference hardware;
2011-09-18, by wenzelm
updated to SML/NJ 110.73;
2011-09-18, by wenzelm
tentative announcement based on current NEWS;
2011-09-18, by wenzelm
tuned;
2011-09-18, by wenzelm
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
2011-09-18, by wenzelm
updated for release;
2011-09-18, by wenzelm
tuned;
2011-09-18, by wenzelm
updated generated file;
2011-09-18, by wenzelm
updated Complete_Lattices;
2011-09-18, by wenzelm
some tuning and re-ordering for release;
2011-09-18, by wenzelm
misc tuning for release;
2011-09-18, by wenzelm
more contributors;
2011-09-18, by wenzelm
tuned proofs;
2011-09-18, by wenzelm
tweak keyboard shortcuts for Mac OS X;
2011-09-18, by wenzelm
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
2011-09-18, by wenzelm
finite sequences as useful as introductory example;
2011-09-18, by wenzelm
discontinued hard-wired JAVA_HOME treatment for Mac OS X (cf. f471a2fb9a95), which can cause confusions of "isabelle java" vs. "isabelle scala" -- moved settings to external component;
2011-09-18, by wenzelm
graph traversal in topological order;
2011-09-18, by wenzelm
Document.Node.Name convenience;
2011-09-17, by wenzelm
more precise painting;
2011-09-17, by wenzelm
more elaborate Node_Renderer, which paints node_name.theory only;
2011-09-17, by wenzelm
raised default log level -- to avoid confusing warning about scala.tools.nsc.plugins.Plugin, which is mistaken as jEdit plugin;
2011-09-17, by wenzelm
tuned signature;
2011-09-17, by wenzelm
more careful traversal of theory dependencies to retain standard import order;
2011-09-17, by wenzelm
sane default for class Thy_Load;
2011-09-17, by wenzelm
removed obsolete patches for PG 4.1;
2011-09-17, by wenzelm
specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;
2011-09-17, by wenzelm
added "isabelle scalac" convenience;
2011-09-17, by wenzelm
Symbol.explode as in ML;
2011-09-17, by wenzelm
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
2011-09-17, by wenzelm
dropped unused argument – avoids problem with SML/NJ
2011-09-17, by haftmann
tuned spacing
2011-09-17, by haftmann
tuned
2011-09-17, by haftmann
tuned post fixpoint setup
2011-09-17, by nipkow
merged
2011-09-17, by nipkow
when applying induction rules, remove names of assumptions that come
2011-09-16, by nipkow
remove stray "using [[simp_trace]]"
2011-09-16, by noschinl
tune indenting
2011-09-16, by noschinl
removed unused legacy lemma names, some comment cleanup.
2011-09-16, by kleing
removed word_neq_0_conv from simpset, it's almost never wanted.
2011-09-16, by kleing
removed further legacy rules from Complete_Lattices
2011-09-15, by hoelzl
NEWS on Complete_Lattices, Lattices
2011-09-15, by noschinl
tail recursive proof preprocessing (needed for huge proofs)
2011-09-15, by blanchet
tuning
2011-09-15, by blanchet
merged
2011-09-15, by nipkow
revised AbsInt and added widening and narrowing
2011-09-15, by nipkow
updated comment
2011-09-14, by haftmann
updated generated code
2011-09-14, by haftmann
tuned
2011-09-13, by haftmann
renamed Complete_Lattices lemmas, removed legacy names
2011-09-14, by hoelzl
merged
2011-09-14, by noschinl
create central list for language extensions used by the haskell code generator
2011-09-14, by noschinl
observe distinction between sets and predicates
2011-09-14, by boehmes
merged
2011-09-14, by nipkow
cleand up AbsInt fixpoint iteration; tuned syntax
2011-09-14, by nipkow
tuned proofs
2011-09-13, by huffman
tuned proofs
2011-09-13, by huffman
remove some redundant [simp] declarations;
2011-09-13, by huffman
tune proofs
2011-09-13, by noschinl
tune simpset for Complete_Lattices
2011-09-13, by noschinl
merged
2011-09-13, by bulwahn
added lemma motivated by a more specific lemma in the AFP-KBPs theories
2011-09-13, by bulwahn
simplified unsound proof detection by removing impossible case
2011-09-13, by blanchet
correcting NEWS
2011-09-13, by bulwahn
correcting theory name and dependencies
2011-09-13, by bulwahn
renamed AList_Impl to AList
2011-09-13, by bulwahn
fastsimp -> fastforce in doc
2011-09-13, by nipkow
fix typo
2011-09-12, by huffman
shorten proof of frontier_straddle
2011-09-12, by huffman
NEWS and CONTRIBUTORS
2011-09-12, by huffman
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-12, by huffman
simplify proofs using LIMSEQ lemmas
2011-09-12, by huffman
remove trivial lemma Lim_at_iff_LIM
2011-09-12, by huffman
fix typos
2011-09-12, by huffman
NEWS for euclidean_space class
2011-09-12, by huffman
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
2011-09-12, by huffman
adding NEWS and CONTRIBUTORS
2011-09-12, by hoelzl
merged
2011-09-12, by bulwahn
correcting imports after splitting and renaming AssocList
2011-09-12, by bulwahn
tuned
2011-09-12, by bulwahn
moving connection of association lists to Mappings into a separate theory
2011-09-12, by bulwahn
adding NEWS and CONTRIBUTORS
2011-09-12, by bulwahn
tuned some symbol that probably went there by some strange encoding issue
2011-09-12, by bulwahn
added my contributions to NEWS and CONTRIBUTORS
2011-09-12, by blanchet
fixed type intersection (again)
2011-09-12, by blanchet
consistent option naming
2011-09-12, by blanchet
NEWS fastsimp -> fastforce
2011-09-12, by nipkow
new fastforce replacing fastsimp - less confusing name
2011-09-12, by nipkow
merged
2011-09-11, by wenzelm
NEWS for Library/Product_Lattice.thy
2011-09-11, by huffman
misc tuning and clarification;
2011-09-11, by wenzelm
merged
2011-09-11, by wenzelm
merged
2011-09-11, by huffman
tuned proofs
2011-09-11, by huffman
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
2011-09-11, by huffman
more CONTRIBUTORS;
2011-09-11, by wenzelm
persistent ISABELLE_INTERFACE_CHOICE;
2011-09-11, by wenzelm
explicit choice of interface;
2011-09-11, by wenzelm
more orthogonal signature;
2011-09-11, by wenzelm
updates for release;
2011-09-11, by wenzelm
misc tuning and clarification (NB: settings are already local for named snapshots/releases);
2011-09-11, by wenzelm
some updates of PLATFORMS;
2011-09-11, by wenzelm
more README;
2011-09-11, by wenzelm
merged
2011-09-10, by wenzelm
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
2011-09-10, by krauss
misc tuning;
2011-09-10, by wenzelm
misc tuning and clarification;
2011-09-10, by wenzelm
speed up slow proof;
2011-09-10, by wenzelm
merged
2011-09-10, by wenzelm
more modularization
2011-09-10, by haftmann
stronger colors (as background);
2011-09-10, by wenzelm
some color scheme for theory status;
2011-09-10, by wenzelm
some keyboard shortcuts for important actions;
2011-09-10, by wenzelm
explicit jEdit actions -- to enable key mappings, for example;
2011-09-10, by wenzelm
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
2011-09-10, by wenzelm
tuned usage;
2011-09-10, by wenzelm
simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);
2011-09-10, by wenzelm
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
2011-09-10, by haftmann
fixed definition of type intersection (soundness bug)
2011-09-10, by blanchet
continue with minimization in debug mode in spite of unsoundness
2011-09-10, by blanchet
generalize lemma of_nat_number_of_eq to class number_semiring
2011-09-09, by huffman
merged
2011-09-09, by bulwahn
stating more explicitly our expectation that these two terms have the same term structure
2011-09-09, by bulwahn
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
2011-09-09, by bulwahn
made SML/NJ happy
2011-09-09, by blanchet
call ghc with -XEmptyDataDecls
2011-09-08, by noschinl
merged
2011-09-09, by nipkow
tuned headers
2011-09-09, by nipkow
Library/Saturated.thy: number_semiring class instance
2011-09-08, by huffman
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
2011-09-08, by huffman
merged
2011-09-08, by huffman
remove unnecessary intermediate lemmas
2011-09-08, by huffman
added syntactic classes for "inf" and "sup"
2011-09-09, by krauss
prove existence, uniqueness, and other properties of complex arg function
2011-09-08, by huffman
tuned
2011-09-08, by huffman
remove obsolete intermediate lemma complex_inverse_complex_split
2011-09-08, by huffman
tuned
2011-09-08, by huffman
merged
2011-09-08, by haftmann
tuned
2011-09-08, by haftmann
merged
2011-09-08, by haftmann
merged
2011-09-07, by haftmann
merged
2011-09-06, by haftmann
merged
2011-09-06, by haftmann
merged
2011-09-06, by haftmann
tuned
2011-09-05, by haftmann
merged
2011-09-05, by haftmann
tuned
2011-09-05, by haftmann
tuned
2011-09-04, by haftmann
fixed computation of "in_conj" for polymorphic encodings
2011-09-08, by blanchet
add some new lemmas about cis and rcis;
2011-09-07, by huffman
Complex.thy: move theorems into appropriate subsections
2011-09-07, by huffman
merged
2011-09-07, by huffman
remove redundant lemma complex_of_real_minus_one
2011-09-07, by huffman
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
2011-09-07, by huffman
removed unused lemma sin_cos_squared_add2_mult
2011-09-07, by huffman
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
2011-09-07, by huffman
avoid using legacy theorem names
2011-09-07, by huffman
merged
2011-09-08, by wenzelm
theory of saturated naturals contributed by Peter Gammie
2011-09-07, by haftmann
theory of saturated naturals contributed by Peter Gammie
2011-09-07, by haftmann
lemmas about +, *, min, max on nat
2011-09-07, by haftmann
update Sledgehammer docs
2011-09-07, by blanchet
added new tagged encodings to Metis tests
2011-09-07, by blanchet
also implemented ghost version of the tagged encodings
2011-09-07, by blanchet
added new guards encoding to test
2011-09-07, by blanchet
smarter explicit apply business
2011-09-07, by blanchet
started work on ghost type arg encoding
2011-09-07, by blanchet
stricted type encoding parsing
2011-09-07, by blanchet
more substructural sharing to gain significant compression;
2011-09-08, by wenzelm
XML.cache for partial sharing (strings only);
2011-09-07, by wenzelm
platform-specific look and feel;
2011-09-07, by wenzelm
more README;
2011-09-07, by wenzelm
clarified terminology;
2011-09-07, by wenzelm
no print_state for final proof commands, which return to theory state;
2011-09-07, by wenzelm
NEWS on IsabelleText font;
2011-09-07, by wenzelm
explicit join_syntax ensures command transaction integrity of 'theory';
2011-09-07, by wenzelm
some updates for release;
2011-09-07, by wenzelm
some tuning for release;
2011-09-07, by wenzelm
updated file locations;
2011-09-07, by wenzelm
merged
2011-09-07, by wenzelm
merged
2011-09-07, by bulwahn
removing previously used function locally_monomorphic in the code generator
2011-09-07, by bulwahn
setting const_sorts to false in the type inference of the code generator
2011-09-07, by bulwahn
adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
2011-09-07, by bulwahn
removing previous crude approximation to add type annotations to disambiguate types
2011-09-07, by bulwahn
adding minimalistic implementation for printing the type annotations
2011-09-07, by bulwahn
adding call to disambiguation annotations
2011-09-07, by bulwahn
adding type inference for disambiguation annotations in code equation
2011-09-07, by bulwahn
adding the body type as well to the code generation for constants as it is required for type annotations of constants
2011-09-07, by bulwahn
changing const type to pass along if typing annotations are necessary for disambigous terms
2011-09-07, by bulwahn
fixed THF type constructor syntax
2011-09-07, by blanchet
tweaking polymorphic TFF and THF output
2011-09-07, by blanchet
parse new experimental '@' encodings
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
clarified import;
2011-09-07, by wenzelm
tuned/simplified proofs;
2011-09-07, by wenzelm
tuned proofs;
2011-09-07, by wenzelm
deactivate unfinished charset provider for now, to avoid user confusion;
2011-09-07, by wenzelm
more NEWS;
2011-09-07, by wenzelm
added "check" button: adhoc change to full buffer perspective;
2011-09-07, by wenzelm
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
2011-09-07, by wenzelm
separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
2011-09-07, by blanchet
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-09-07, by blanchet
tuning
2011-09-07, by blanchet
make mangling sound w.r.t. type arguments
2011-09-07, by blanchet
make "filter_type_args" more robust if the actual arity is higher than the declared one
2011-09-07, by blanchet
updated Sledgehammer documentation
2011-09-07, by blanchet
rationalize uniform encodings
2011-09-07, by blanchet
merged
2011-09-06, by huffman
avoid using legacy theorem names
2011-09-06, by huffman
merged
2011-09-06, by huffman
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
2011-09-06, by huffman
HOL/Import: Update HOL4 generated files to current Isabelle.
2011-09-07, by Cezary Kaliszyk
tuned proofs;
2011-09-07, by wenzelm
remove some unnecessary simp rules from simpset
2011-09-06, by huffman
some Isabelle/jEdit NEWS;
2011-09-06, by wenzelm
more README;
2011-09-06, by wenzelm
merged
2011-09-06, by wenzelm
merged
2011-09-06, by huffman
simplify proof of tan_half, removing unused assumptions
2011-09-06, by huffman
convert some proofs to Isar-style
2011-09-06, by huffman
added dummy polymorphic THF system
2011-09-06, by blanchet
added some examples for pattern and weight annotations
2011-09-06, by boehmes
merged
2011-09-06, by bulwahn
avoid "Code" as structure name (cf. 3bc39cfe27fe)
2011-09-06, by bulwahn
remove duplicate copy of lemma sqrt_add_le_add_sqrt
2011-09-06, by huffman
remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-06, by huffman
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
2011-09-06, by huffman
merged
2011-09-06, by huffman
add lemmas about arctan;
2011-09-05, by huffman
convert lemma cos_total to Isar-style proof
2011-09-05, by huffman
added new lemmas
2011-09-06, by nipkow
updated Sledgehammer's docs
2011-09-06, by blanchet
cleanup "simple" type encodings
2011-09-06, by blanchet
merge
2011-09-06, by Cezary Kaliszyk
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
2011-09-06, by Cezary Kaliszyk
tuning
2011-09-06, by blanchet
drop more type arguments soundly, when they can be deduced from the arg types
2011-09-06, by blanchet
bulk reports for improved message throughput;
2011-09-06, by wenzelm
bulk reports for improved message throughput;
2011-09-06, by wenzelm
tuned signature;
2011-09-06, by wenzelm
more specific message channels to avoid potential bottle-neck of raw_messages;
2011-09-06, by wenzelm
buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
2011-09-06, by wenzelm
more abstract receiver interface;
2011-09-06, by wenzelm
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
2011-09-06, by wenzelm
convert lemma cos_is_zero to Isar-style
2011-09-05, by huffman
merged
2011-09-05, by huffman
convert lemma sin_gt_zero to Isar style;
2011-09-05, by huffman
modify lemma sums_group, and shorten proofs that use it
2011-09-05, by huffman
generalize some lemmas
2011-09-05, by huffman
add lemmas cos_arctan and sin_arctan
2011-09-05, by huffman
tuned indentation
2011-09-05, by huffman
more visible outdated_color;
2011-09-05, by wenzelm
commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
2011-09-05, by wenzelm
tuned imports;
2011-09-05, by wenzelm
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
2011-09-05, by blanchet
tuned
2011-09-05, by boehmes
tuned
2011-09-05, by boehmes
filter out all schematic theorems if the problem contains no ground constants
2011-09-05, by boehmes
merged
2011-09-04, by huffman
tuned comments
2011-09-04, by huffman
simplify proof of Bseq_mono_convergent
2011-09-04, by huffman
merged
2011-09-04, by wenzelm
replace lemma expi_imaginary with reoriented lemma cis_conv_exp
2011-09-04, by huffman
remove redundant lemmas expi_add and expi_zero
2011-09-04, by huffman
remove redundant lemmas about LIMSEQ
2011-09-04, by huffman
introduce abbreviation 'int' earlier in Int.thy
2011-09-04, by huffman
remove unused assumptions from natceiling lemmas
2011-09-04, by huffman
move lemmas nat_le_iff and nat_mono into Int.thy
2011-09-04, by huffman
eliminated markup for plain identifiers (frequent but insignificant);
2011-09-04, by wenzelm
simplified signatures;
2011-09-04, by wenzelm
synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
2011-09-04, by wenzelm
tuned document;
2011-09-04, by wenzelm
improved handling of extended styles and hard tabs when prover is inactive;
2011-09-04, by wenzelm
mark hard tabs as single chunks, as required by jEdit;
2011-09-04, by wenzelm
updated READMEs;
2011-09-04, by wenzelm
property "tooltip-dismiss-delay" is edited in ms, not seconds;
2011-09-04, by wenzelm
moved XML/YXML to src/Pure/PIDE;
2011-09-04, by wenzelm
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
2011-09-04, by wenzelm
pseudo-definition for perms on sets; tuned
2011-09-04, by haftmann
remove duplicate lemma nat_zero in favor of nat_0
2011-09-03, by huffman
merged
2011-09-03, by huffman
merged
2011-09-03, by huffman
modify nominal packages to better respect set/pred distinction
2011-09-03, by huffman
merged
2011-09-03, by huffman
remove unused assumption from lemma posreal_complete
2011-09-03, by huffman
tuned specifications
2011-09-03, by haftmann
merged
2011-09-03, by haftmann
tuned proof
2011-09-03, by haftmann
merged
2011-09-03, by haftmann
assert Pure equations for theorem references; avoid dynamic reference to fact
2011-09-03, by haftmann
assert Pure equations for theorem references; tuned
2011-09-03, by haftmann
tuned specifications and proofs
2011-09-03, by haftmann
merged
2011-09-03, by wenzelm
remove duplicate lemma finite_choice in favor of finite_set_choice
2011-09-03, by huffman
simplify proof
2011-09-03, by huffman
shorten some proofs
2011-09-03, by huffman
remove redundant simp rules ceiling_floor and floor_ceiling
2011-09-02, by huffman
misc tuning and simplification of proofs;
2011-09-03, by wenzelm
Document.removed_versions on Scala side;
2011-09-03, by wenzelm
discontinued predefined empty command (obsolete!?);
2011-09-03, by wenzelm
discontinued global execs: store exec value directly within entries;
2011-09-03, by wenzelm
Document.remove_versions on ML side;
2011-09-03, by wenzelm
some support to prune_history;
2011-09-03, by wenzelm
merged
2011-09-02, by huffman
speed up extremely slow metis proof of Sup_real_iff
2011-09-02, by huffman
remove redundant lemma reals_complete2 in favor of complete_real
2011-09-02, by huffman
simplify proof of Rats_dense_in_real;
2011-09-02, by huffman
remove unused, unnecessary lemmas
2011-09-02, by huffman
remove more duplicate lemmas
2011-09-02, by huffman
merged
2011-09-02, by wenzelm
merged
2011-09-02, by haftmann
avoid "Code" as structure name
2011-09-02, by haftmann
more robust chunk painting wrt. hard tabs, when chunk.str == null;
2011-09-02, by wenzelm
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
2011-09-02, by wenzelm
less agressive parsing of commands (priority ~1);
2011-09-02, by wenzelm
tuned;
2011-09-02, by wenzelm
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-09-02, by wenzelm
merged
2011-09-02, by nipkow
Added Abstract Interpretation theories
2011-09-02, by nipkow
tuned proofs;
2011-09-02, by wenzelm
proper config option linarith_trace;
2011-09-02, by wenzelm
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
2011-09-02, by wenzelm
merged
2011-09-02, by wenzelm
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-09-02, by blanchet
use new syntax for Pi binder in TFF1 output
2011-09-02, by blanchet
fewer TPTP important messages
2011-09-02, by blanchet
simplify some proofs about uniform continuity, and add some new ones;
2011-09-01, by huffman
modernize lemmas about 'continuous' and 'continuous_on';
2011-09-01, by huffman
add lemma tendsto_infnorm
2011-09-01, by huffman
more precise iterate_entries_after if start refers to last entry;
2011-09-02, by wenzelm
clarified define_command: store name as structural information;
2011-09-02, by wenzelm
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
2011-09-01, by wenzelm
more redable Document.Node.toString;
2011-09-01, by wenzelm
sort wrt. theory name;
2011-09-01, by wenzelm
modernized theory name;
2011-09-01, by wenzelm
repaired benchmarks;
2011-09-01, by wenzelm
merged
2011-09-01, by wenzelm
tuning
2011-09-01, by blanchet
always measure time for ATPs -- auto minimization relies on it
2011-09-01, by blanchet
added two lemmas about "distinct" to help Sledgehammer
2011-09-01, by blanchet
make "sound" sound and "unsound" more sound, based on evaluation
2011-09-01, by blanchet
HOL/Import: observe distinction between sets and predicates (where possible)
2011-09-01, by Cezary Kaliszyk
simplify/generalize some proofs
2011-08-31, by huffman
generalize lemma isCont_vec_nth
2011-08-31, by huffman
convert proof to Isar-style
2011-08-31, by huffman
remove redundant lemma card_enum
2011-08-31, by huffman
move lemmas from Topology_Euclidean_Space to Euclidean_Space
2011-08-31, by huffman
convert to Isar-style proof
2011-08-31, by huffman
make SML/NJ happy
2011-08-31, by blanchet
more tuning
2011-08-31, by blanchet
more tuning
2011-08-31, by blanchet
tuning
2011-08-31, by blanchet
avoid relying on dubious TFF1 feature
2011-08-31, by blanchet
killed FIXME (the ATP exporter outputs TPTP FOF, which is first-order)
2011-08-31, by blanchet
fixed explicit declaration of TFF1 types
2011-08-31, by blanchet
adding list_size_append (thanks to Rene Thiemann)
2011-08-30, by bulwahn
strengthening list_size_pointwise (thanks to Rene Thiemann)
2011-08-30, by bulwahn
more flexible sorting;
2011-09-01, by wenzelm
tuned signature;
2011-09-01, by wenzelm
more abstract Document.Node.Name;
2011-09-01, by wenzelm
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
2011-09-01, by wenzelm
crude display of node status;
2011-08-31, by wenzelm
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
2011-08-31, by wenzelm
explicit running_color;
2011-08-31, by wenzelm
tuned join_commands: avoid traversing cumulative table;
2011-08-31, by wenzelm
some support for theory status overview;
2011-08-31, by wenzelm
tuned Commands_Changed: cover nodes as well;
2011-08-31, by wenzelm
maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-31, by wenzelm
improved auto loading: selectable file list;
2011-08-31, by wenzelm
tuned document;
2011-08-30, by wenzelm
tuned import;
2011-08-30, by wenzelm
tuned document;
2011-08-30, by wenzelm
tuned color for Mac OS X (very light color profile?);
2011-08-30, by wenzelm
tuned document;
2011-08-30, by wenzelm
merged;
2011-08-30, by wenzelm
fixed just introduced silly bug
2011-08-30, by blanchet
"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
2011-08-30, by blanchet
tuning
2011-08-30, by blanchet
cleaner "pff" dummy TFF0 prover
2011-08-30, by blanchet
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
2011-08-30, by blanchet
added type abstractions (for declaring polymorphic constants) to TFF syntax
2011-08-30, by blanchet
implement more of the polymorphic simply typed format TFF(1)
2011-08-30, by blanchet
flip logic of boolean option so it's off by default
2011-08-30, by blanchet
extended simple types with polymorphism -- the implementation still needs some work though
2011-08-30, by blanchet
added dummy PFF prover, for debugging purposes
2011-08-30, by blanchet
first step towards polymorphic TFF + changed defaults for Vampire
2011-08-30, by blanchet
tuning
2011-08-30, by blanchet
removed explicit reliance on Hilbert_Choice.Eps
2011-08-30, by nik
improved handling of induction rules in Sledgehammer
2011-08-30, by nik
added generation of induction rules
2011-08-30, by nik
simplify some proofs
2011-08-29, by huffman
restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);
2011-08-30, by wenzelm
tuned signature;
2011-08-30, by wenzelm
dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);
2011-08-30, by wenzelm
some support for hyperlinks between different buffers;
2011-08-30, by wenzelm
tuned colors -- more distance between outdated_color and quoted_color;
2011-08-30, by wenzelm
do not normalized extra file dependencies for now -- still loaded by prover process;
2011-08-30, by wenzelm
separate module for jEdit primitives for loading theory files;
2011-08-30, by wenzelm
merged
2011-08-29, by wenzelm
Product_Vector.thy: clean up some proofs
2011-08-29, by huffman
actual auto loading of required files;
2011-08-29, by wenzelm
some dialog for auto loading of required files (still inactive);
2011-08-29, by wenzelm
invoke in Swing thread to make double sure;
2011-08-29, by wenzelm
move class perfect_space into RealVector.thy;
2011-08-28, by huffman
generalize LIM_zero lemmas to arbitrary filters
2011-08-28, by huffman
merged
2011-08-28, by huffman
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-28, by huffman
tuned
2011-08-28, by haftmann
split timeout among ATPs in and add Metis to the mix as backup
2011-08-28, by blanchet
more portable cp options, e.g. for non-GNU version on Mac OS X Leopard;
2011-08-28, by wenzelm
tuned positions of ambiguity messages -- less intrusive in IDE view;
2011-08-28, by wenzelm
tuned
2011-08-28, by haftmann
merged
2011-08-28, by haftmann
avoid loading List_Cset and Dlist_Cet at the same time
2011-08-28, by haftmann
corrected slip
2011-08-28, by haftmann
Cset, Dlist_Cset, List_Cset: restructured
2011-08-27, by haftmann
Cset, Dlist_Cset, List_Cset: restructured
2011-08-27, by haftmann
adapted to changes in Cset.thy
2011-08-27, by haftmann
adapted to changes in Cset.thy
2011-08-26, by haftmann
separating predicates and sets syntactically
2011-08-26, by haftmann
merged
2011-08-26, by haftmann
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
2011-08-26, by haftmann
updated generated files
2011-08-25, by haftmann
merged
2011-08-25, by haftmann
updated generated files
2011-08-25, by haftmann
explicit markup for legacy warnings;
2011-08-27, by wenzelm
updated generated files;
2011-08-27, by wenzelm
less aggressive warning icon;
2011-08-27, by wenzelm
tuned colors;
2011-08-27, by wenzelm
transparent foreground color for quoted entities;
2011-08-27, by wenzelm
more precise treatment of nodes that are fully required for partially visible ones;
2011-08-27, by wenzelm
de-assigned commands also count as changed;
2011-08-27, by wenzelm
beef up sledgehammer_tac in Mirabelle some more
2011-08-27, by blanchet
merged
2011-08-27, by blanchet
change default for generation of tag idempotence and tag argument equations
2011-08-26, by blanchet
merged
2011-08-26, by huffman
NEWS entry for setsum_norm ~> norm_setsum
2011-08-26, by huffman
make HOL-Probability respect set/pred distinction
2011-08-26, by huffman
merged
2011-08-26, by wenzelm
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
2010-09-08, by huffman
merged
2011-08-26, by huffman
generalize and simplify proof of continuous_within_sequentially
2011-08-26, by huffman
add lemma sequentially_imp_eventually_within;
2011-08-26, by huffman
replace some continuous_on lemmas with more general versions
2011-08-25, by huffman
remove legacy theorem Lim_inner
2011-08-25, by huffman
arrange everything related to ordered_euclidean_space class together
2011-08-25, by huffman
generalize and shorten proof of basis_orthogonal
2011-08-25, by huffman
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
2011-08-25, by huffman
merged
2011-08-25, by huffman
generalize lemma finite_imp_compact_convex_hull and related lemmas
2011-08-25, by huffman
generalize some lemmas
2011-08-25, by huffman
generalize lemma convex_cone_hull
2011-08-25, by huffman
rename subset_{interior,closure} to {interior,closure}_mono;
2011-08-25, by huffman
simplify many proofs about subspace and span;
2011-08-25, by huffman
remove duplicate simp declaration
2011-08-25, by huffman
simplify definition of 'interior';
2011-08-25, by huffman
add lemma closure_union;
2011-08-24, by huffman
minimize imports
2011-08-24, by huffman
move everything related to 'norm' method into new theory file Norm_Arith.thy
2011-08-24, by huffman
remove unused lemmas dimensionI, dimension_eq
2011-08-24, by huffman
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
2011-08-24, by huffman
merge
2011-08-26, by Cezary Kaliszyk
FSet: Explicit proof without mem_def
2011-08-26, by Cezary Kaliszyk
merged
2011-08-26, by nipkow
added lemma
2011-08-26, by nipkow
added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files
2011-08-26, by blanchet
comment
2011-08-26, by blanchet
disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
2011-08-26, by blanchet
improve completeness of polymorphic encodings
2011-08-26, by blanchet
mangle tag bound declarations properly
2011-08-26, by blanchet
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
2011-08-26, by blanchet
make sure that if slicing is disabled, a non-SOS slice is chosen
2011-08-25, by blanchet
honor TFF Implicit
2011-08-25, by blanchet
make polymorphic encodings more complete
2011-08-25, by blanchet
make default unsound mode less unsound
2011-08-25, by blanchet
make TFF output less explicit where possible
2011-08-25, by blanchet
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
2011-08-25, by blanchet
added one more known Z3 failure
2011-08-25, by blanchet
added config options to control two aspects of the translation, for evaluation purposes
2011-08-25, by blanchet
added choice operator output for
2011-08-25, by nik
rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-25, by blanchet
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
2011-08-25, by blanchet
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
2011-08-25, by blanchet
fixed bang encoding detection of which types to encode
2011-08-25, by blanchet
lemma Compl_insert: "- insert x A = (-A) - {x}"
2011-08-25, by krauss
avoid variable clashes by properly incrementing indices
2011-08-25, by boehmes
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
2011-08-25, by boehmes
include chained facts for minimizer, otherwise it won't work
2011-08-25, by blanchet
remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
2011-08-24, by blanchet
back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
2011-08-26, by wenzelm
tuned Session.edit_node: update_perspective based on last_exec_offset;
2011-08-26, by wenzelm
tuned signature -- iterate subsumes both fold and get_first;
2011-08-26, by wenzelm
further clarification of Document.updated, based on last_common and after_entry;
2011-08-26, by wenzelm
tuned signature;
2011-08-26, by wenzelm
improved Document.edit: more accurate update_start and no_execs;
2011-08-26, by wenzelm
refined document state assignment: observe perspective, more explicit assignment message;
2011-08-26, by wenzelm
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-25, by wenzelm
maintain last_execs assignment on Scala side;
2011-08-25, by wenzelm
propagate information about last command with exec state assignment through document model;
2011-08-25, by wenzelm
tuned signature;
2011-08-25, by wenzelm
slightly more abstract Command.Perspective;
2011-08-25, by wenzelm
slightly more abstract Text.Perspective;
2011-08-25, by wenzelm
tuned proofs;
2011-08-24, by wenzelm
tuned syntax -- avoid ambiguities;
2011-08-24, by wenzelm
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
2011-08-24, by wenzelm
delete commented-out dead code
2011-08-24, by huffman
merged
2011-08-24, by huffman
change some subsection headings to subsubsection
2011-08-24, by huffman
remove unnecessary lemma card_ge1
2011-08-23, by huffman
move connected_real_lemma to the one place it is used
2011-08-23, by huffman
merged
2011-08-24, by wenzelm
make sure that all facts are passed to ATP from minimizer
2011-08-24, by blanchet
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
2011-08-24, by blanchet
specify timeout for "sledgehammer_tac"
2011-08-24, by blanchet
tuning
2011-08-24, by blanchet
Quotient Package: add mem_rsp, mem_prs, tune proofs.
2011-08-24, by Cezary Kaliszyk
merged
2011-08-23, by huffman
declare euclidean_simps [simp] at the point they are proved;
2011-08-23, by huffman
merged
2011-08-23, by huffman
merged
2011-08-22, by huffman
avoid warnings
2011-08-22, by huffman
comment out dead code to avoid compiler warnings
2011-08-22, by huffman
legacy theorem names
2011-08-22, by huffman
remove duplicate lemma
2011-08-22, by huffman
fixed "hBOOL" of existential variables, and generate more helpers
2011-08-23, by blanchet
don't select facts when using sledgehammer_tac for reconstruction
2011-08-23, by blanchet
don't perform a triviality check if the goal is skipped anyway
2011-08-23, by blanchet
optional reconstructor
2011-08-23, by blanchet
misc tuning and simplification;
2011-08-24, by wenzelm
tuned pri: prefer purging of canceled execution;
2011-08-24, by wenzelm
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
2011-08-24, by wenzelm
clarified Document.Node.clear -- retain header (cf. ML version);
2011-08-24, by wenzelm
clarified norm_header/header_edit -- disallow update of loaded theories;
2011-08-24, by wenzelm
misc tuning and simplification;
2011-08-24, by wenzelm
ignore irrelevant timings;
2011-08-24, by wenzelm
print state only for visible command, to avoid wasting resources for the larger part of the text;
2011-08-24, by wenzelm
early filtering of unchanged perspective;
2011-08-24, by wenzelm
more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
2011-08-24, by wenzelm
update_perspective without actual edits, bypassing the full state assignment protocol;
2011-08-24, by wenzelm
tuned;
2011-08-23, by wenzelm
handle potentially more approriate BufferUpdate.LOADED event;
2011-08-23, by wenzelm
special treatment of structure index 1 in Pure, including legacy warning;
2011-08-22, by wenzelm
compile
2011-08-23, by blanchet
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
2011-08-23, by blanchet
beef up "sledgehammer_tac" reconstructor
2011-08-23, by blanchet
clean up Sledgehammer tactic
2011-08-23, by blanchet
fixed document;
2011-08-23, by wenzelm
tuned signature;
2011-08-23, by wenzelm
merged
2011-08-23, by wenzelm
always use TFF if possible
2011-08-23, by blanchet
clearer separator in generated file names
2011-08-23, by blanchet
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
2011-08-23, by blanchet
updated known failures for Z3 3.0 TPTP
2011-08-23, by blanchet
updated Z3 docs
2011-08-23, by blanchet
avoid TFF format with older Vampire versions
2011-08-23, by blanchet
update the Vampire related parts of the documentation
2011-08-23, by blanchet
fixed TFF slicing
2011-08-23, by blanchet
kindly ask Vampire to output axiom names
2011-08-23, by blanchet
added formats to the slice and use TFF for remote Vampire
2011-08-23, by blanchet
tuned specifications, syntax and proofs
2011-08-23, by haftmann
tuned specifications and syntax
2011-08-22, by haftmann
Quotient Package: some infrastructure for lifting inside sets
2011-08-23, by Cezary Kaliszyk
include all encodings in tests, now that the incompleteness of some encodings has been addressed
2011-08-22, by blanchet
change Metis's default settings if type information axioms are generated
2011-08-22, by blanchet
we must tag any type whose ground types intersect a nonmonotonic type
2011-08-22, by blanchet
prefer the lighter, slightly unsound monotonicity-based encodings for Metis
2011-08-22, by blanchet
made reconstruction of type tag equalities "\?x = \?x" reliable
2011-08-22, by blanchet
tuning ATP problem output
2011-08-22, by blanchet
revert guard logic -- make sure that typing information is generated for existentials
2011-08-22, by blanchet
generate tag equations for existential variables
2011-08-22, by blanchet
tuning, plus started implementing tag equation generation for existential variables
2011-08-22, by blanchet
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
2011-08-22, by blanchet
clearer terminology
2011-08-22, by blanchet
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
2011-08-22, by blanchet
removed unused configuration option
2011-08-22, by blanchet
added caching for (in)finiteness checks
2011-08-22, by blanchet
remove needless typing information
2011-08-22, by blanchet
cleaner handling of polymorphic monotonicity inference
2011-08-22, by blanchet
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
2011-08-22, by blanchet
more precise warning
2011-08-22, by blanchet
added option to control soundness of encodings more precisely, for evaluation purposes
2011-08-22, by blanchet
make sound mode more sound (and clean up code)
2011-08-22, by blanchet
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
2011-08-22, by blanchet
gracefully handle empty SPASS problems
2011-08-22, by blanchet
pass sound option to Sledgehammer tactic
2011-08-22, by blanchet
tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-08-23, by wenzelm
tuned signature;
2011-08-23, by wenzelm
discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);
2011-08-23, by wenzelm
some support for toplevel printing wrt. editor perspective (still inactive);
2011-08-23, by wenzelm
propagate editor perspective through document model;
2011-08-23, by wenzelm
some support for editor perspective;
2011-08-22, by wenzelm
discontinued redundant Edit_Command_ID;
2011-08-22, by wenzelm
reduced warnings;
2011-08-22, by wenzelm
tuned message;
2011-08-22, by wenzelm
old-style numbered structure index is legacy feature (hardly ever used now);
2011-08-22, by wenzelm
added official Text.Range.Ordering;
2011-08-22, by wenzelm
tuned signature;
2011-08-22, by wenzelm
reverted some odd changes to HOL/Import (cf. 74c08021ab2e);
2011-08-22, by wenzelm
merged
2011-08-22, by krauss
modernized specifications
2011-08-21, by krauss
removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
2011-08-21, by krauss
removed technical or trivial unused facts
2011-08-21, by krauss
more precise authors and comments;
2011-08-21, by krauss
added proof of idempotence, roughly after HOL/Subst/Unify.thy
2011-08-21, by krauss
tuned proofs, sledgehammering overly verbose parts
2011-08-21, by krauss
tuned notation
2011-08-21, by krauss
ported some lemmas from HOL/Subst/*;
2011-08-21, by krauss
changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
2011-08-21, by krauss
merged
2011-08-21, by huffman
add lemmas interior_Times and closure_Times
2011-08-21, by huffman
avoid pred/set mixture
2011-08-21, by haftmann
avoid pred/set mixture
2011-08-21, by haftmann
merged
2011-08-21, by wenzelm
remove unnecessary euclidean_space class constraints
2011-08-21, by huffman
section -> subsection
2011-08-21, by huffman
scale dependency graph to fit on page
2011-08-21, by huffman
more robust initialization of token marker and line context wrt. session startup;
2011-08-21, by wenzelm
tuned Parse.group: delayed failure message;
2011-08-21, by wenzelm
avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
2011-08-21, by wenzelm
default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
2011-08-21, by wenzelm
tuned;
2011-08-21, by wenzelm
discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
2011-08-21, by wenzelm
discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
2011-08-21, by wenzelm
merged
2011-08-21, by wenzelm
replace lemma realpow_two_diff with new lemma square_diff_square_factored
2011-08-20, by huffman
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
2011-08-20, by huffman
move lemma add_eq_0_iff to Groups.thy
2011-08-20, by huffman
remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
2011-08-20, by huffman
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
2011-08-20, by huffman
add lemma power2_eq_iff
2011-08-20, by huffman
remove some over-specific rules from the simpset
2011-08-20, by huffman
merged
2011-08-20, by huffman
redefine constant 'trivial_limit' as an abbreviation
2011-08-20, by huffman
purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
2011-08-21, by wenzelm
refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
2011-08-21, by wenzelm
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
2011-08-20, by wenzelm
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-08-20, by wenzelm
clarified get_imports -- should not rely on accidental order within graph;
2011-08-20, by wenzelm
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
2011-08-20, by wenzelm
discontinued "Interrupt", which could disturb administrative tasks of the document model;
2011-08-20, by wenzelm
more direct balanced version Ord_List.unions;
2011-08-20, by wenzelm
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
2011-08-20, by wenzelm
tuned future priorities (again);
2011-08-20, by wenzelm
clarified fulfill_norm_proof: no join_thms yet;
2011-08-20, by wenzelm
added Future.joins convenience;
2011-08-20, by wenzelm
merged
2011-08-20, by haftmann
deactivated »unknown« nitpick example
2011-08-20, by haftmann
merged
2011-08-20, by haftmann
tuned proof
2011-08-20, by haftmann
more uniform formatting of specifications
2011-08-20, by haftmann
compatibility layer
2011-08-20, by haftmann
merged
2011-08-20, by haftmann
more concise definition for Inf, Sup on bool
2011-08-19, by haftmann
do not call ghc with -fglasgow-exts
2011-08-18, by noschinl
remove some redundant simp rules about sqrt
2011-08-19, by huffman
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
2011-08-19, by huffman
remove unused lemma DERIV_sin_add
2011-08-19, by huffman
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
2011-08-19, by huffman
remove redundant lemma exp_ln_eq in favor of ln_unique
2011-08-19, by huffman
merged
2011-08-19, by huffman
Lim.thy: legacy theorems
2011-08-19, by huffman
SEQ.thy: legacy theorem names
2011-08-19, by huffman
delete unused lemmas about limits
2011-08-19, by huffman
Transcendental.thy: add tendsto_intros lemmas;
2011-08-19, by huffman
add lemma isCont_tendsto_compose
2011-08-19, by huffman
merged
2011-08-19, by wenzelm
Transcendental.thy: remove several unused lemmas and simplify some proofs
2011-08-19, by huffman
remove unused lemmas
2011-08-19, by huffman
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
2011-08-19, by huffman
remove some redundant simp rules
2011-08-19, by huffman
maintain recent future proofs at transaction boundaries;
2011-08-19, by wenzelm
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
2011-08-19, by wenzelm
tuned;
2011-08-19, by wenzelm
tuned signature (again);
2011-08-19, by wenzelm
tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19, by wenzelm
refined Future.cancel: explicit future allows to join actual cancellation;
2011-08-19, by wenzelm
Future.promise: explicit abort operation (like uninterruptible future job);
2011-08-19, by wenzelm
editable raw text areas: allow user to clear content;
2011-08-19, by wenzelm
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
2011-08-19, by wenzelm
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
2011-08-19, by wenzelm
clarified Future.cond_forks: more uniform handling of exceptional situations;
2011-08-19, by wenzelm
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
2011-08-19, by Cezary Kaliszyk
merged
2011-08-18, by huffman
define complex exponential 'expi' as abbreviation for 'exp'
2011-08-18, by huffman
remove more bounded_linear locale interpretations (cf. f0de18b62d63)
2011-08-18, by huffman
optimize some proofs
2011-08-18, by huffman
add Multivariate_Analysis dependencies
2011-08-18, by huffman
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
2011-08-18, by huffman
declare euclidean_component_zero[simp] at the point it is proved
2011-08-18, by huffman
Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
2011-08-19, by Cezary Kaliszyk
merged;
2011-08-18, by wenzelm
merged
2011-08-18, by huffman
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-18, by huffman
merged
2011-08-18, by haftmann
merged
2011-08-18, by haftmann
avoid duplicated simp add option
2011-08-18, by haftmann
observe distinction between sets and predicates more properly
2011-08-18, by haftmann
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
2011-08-18, by haftmann
avoid case-sensitive name for example theory
2011-08-18, by haftmann
merged
2011-08-18, by nipkow
case_names NEWS
2011-08-18, by nipkow
adding documentation about simps equation in the inductive package
2011-08-18, by bulwahn
activating narrowing-based quickcheck by default
2011-08-18, by bulwahn
more precise treatment of exception nesting and serial numbers;
2011-08-18, by wenzelm
more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-18, by wenzelm
updated sequential version (cf. b94951f06e48);
2011-08-18, by wenzelm
tuned comments;
2011-08-18, by wenzelm
tuned document;
2011-08-18, by wenzelm
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
2011-08-18, by wenzelm
export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;
2011-08-18, by wenzelm
tune Par_Exn.make: balance merge;
2011-08-18, by wenzelm
Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
2011-08-18, by Cezary Kaliszyk
merged
2011-08-17, by huffman
HOL-IMP: respect set/pred distinction
2011-08-17, by huffman
Determinants.thy: avoid using mem_def/Collect_def
2011-08-17, by huffman
Wfrec.thy: respect set/pred distinction
2011-08-17, by huffman
follow updates of Isabelle/Pure;
2011-08-18, by wenzelm
merged
2011-08-17, by wenzelm
IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
2011-08-17, by huffman
merged
2011-08-17, by huffman
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
2011-08-17, by huffman
add lemma tendsto_compose_eventually; use it to shorten some proofs
2011-08-17, by huffman
Topology_Euclidean_Space.thy: simplify some proofs
2011-08-17, by huffman
add lemma metric_tendsto_imp_tendsto
2011-08-17, by huffman
simplify proofs of lemmas open_interval, closed_interval
2011-08-17, by huffman
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
2011-08-17, by wenzelm
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
2011-08-17, by wenzelm
more systematic handling of parallel exceptions;
2011-08-17, by wenzelm
tuned signature;
2011-08-17, by wenzelm
merged
2011-08-17, by haftmann
merged
2011-08-17, by haftmann
merged
2011-08-17, by haftmann
avoid Collect_def in proof
2011-08-16, by haftmann
modernized signature of Term.absfree/absdummy;
2011-08-17, by wenzelm
improved default context for ML toplevel pretty-printing;
2011-08-17, by wenzelm
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
2011-08-17, by wenzelm
some convenience actions/shortcuts for control symbols;
2011-08-17, by wenzelm
export Function_Fun.fun_config for user convenience;
2011-08-17, by wenzelm
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
2011-08-17, by wenzelm
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
2011-08-17, by blanchet
merged
2011-08-16, by huffman
add simp rules for isCont
2011-08-16, by huffman
updated keywords -- old codegen is no longer in Pure;
2011-08-16, by wenzelm
include HOL-Library keywords for the sake of recdef;
2011-08-16, by wenzelm
merged
2011-08-16, by wenzelm
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
2011-08-16, by huffman
get Multivariate_Analysis/Determinants.thy compiled and working again
2011-08-16, by huffman
get Library/Permutations.thy compiled and working again
2011-08-16, by huffman
workaround for Cygwin, to make it work in the important special case without extra files;
2011-08-16, by wenzelm
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
2011-08-16, by wenzelm
tuned message;
2011-08-16, by wenzelm
more robust treatment of node dependencies in incremental edits;
2011-08-16, by wenzelm
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
2011-08-16, by wenzelm
omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;
2011-08-16, by wenzelm
merged
2011-08-15, by huffman
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
2011-08-15, by huffman
add lemma tendsto_compose
2011-08-15, by huffman
remove extraneous subsection heading
2011-08-15, by huffman
generalized lemma closed_Collect_eq
2011-08-15, by huffman
remove duplicate lemma disjoint_iff
2011-08-15, by huffman
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
2011-08-15, by huffman
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
2011-08-15, by huffman
generalize lemma continuous_uniform_limit to class metric_space
2011-08-15, by huffman
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
2011-08-15, by huffman
Topology_Euclidean_Space.thy: organize section headings
2011-08-15, by huffman
simplify some proofs
2011-08-15, by huffman
generalize lemma convergent_subseq_convergent
2011-08-14, by huffman
locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
2011-08-14, by huffman
locale-ize some constant definitions, so complete_space can inherit from metric_space
2011-08-14, by huffman
generalize constant 'lim' and limit uniqueness theorems to class t2_space
2011-08-14, by huffman
Quotient Package: make quotient_type work with separate set type
2011-08-16, by Cezary Kaliszyk
updated README;
2011-08-15, by wenzelm
touch descendants of edited nodes;
2011-08-15, by wenzelm
parellel scheduling of node edits and execution;
2011-08-15, by wenzelm
tuned error message;
2011-08-15, by wenzelm
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
tuned signature;
2011-07-09, by wenzelm
clarified propagation of node name and header;
2011-07-09, by wenzelm
more precise treatment of prover definedness;
2011-07-09, by wenzelm
tuned source structure;
2011-07-09, by wenzelm
some support for blobs (arbitrary text files) within document nodes;
2011-07-09, by wenzelm
tuned signature;
2011-07-09, by wenzelm
moved global state to structure Document (again);
2011-07-08, by wenzelm
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
2011-07-08, by wenzelm
less stateful outer_syntax;
2011-07-08, by wenzelm
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
2011-07-08, by wenzelm
discontinued special treatment of hard tabulators;
2011-07-08, by wenzelm
eliminated hard tabs;
2011-07-08, by wenzelm
merged
2011-07-08, by wenzelm
merged
2011-07-08, by nipkow
added translation to fix critical pair between abbreviations for surj and ~=
2011-07-07, by nipkow
floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
2011-07-07, by bulwahn
standardized String.concat towards implode;
2011-07-08, by wenzelm
more abstract Thy_Load.load_file/use_file for external theory resources;
2011-07-08, by wenzelm
comment;
2011-07-08, by wenzelm
clarified Thy_Load.digest_file -- read ML files only once;
2011-07-08, by wenzelm
tuned signature;
2011-07-08, by wenzelm
simplified make_option/dest_option;
2011-07-07, by wenzelm
explicit Document.Node.Header, with master_dir and thy_name;
2011-07-07, by wenzelm
explicit indication of type Symbol.Symbol;
2011-07-07, by wenzelm
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
2011-07-07, by wenzelm
merged
2011-07-06, by wenzelm
make SML/NJ happier
2011-07-06, by blanchet
make SML/NJ happy + tuning
2011-07-06, by blanchet
moved ATP dependencies to HOL-Plain, where they belong
2011-07-06, by blanchet
better setup for experimental "z3_atp"
2011-07-06, by blanchet
64bit versions of some mira configurations
2011-07-06, by krauss
removed unused mira configuration
2011-07-06, by krauss
merged
2011-07-06, by bulwahn
tuning options to avoid spurious isabelle test failures
2011-07-06, by bulwahn
clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
2011-07-06, by wenzelm
prefer Synchronized.var;
2011-07-06, by wenzelm
tuned errors;
2011-07-06, by wenzelm
record package: proper configuration options;
2011-07-06, by wenzelm
just one copy of split_args;
2011-07-06, by wenzelm
merged
2011-07-06, by wenzelm
rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
2011-07-05, by hoelzl
improved translation of lambdas in THF
2011-07-05, by nik
added generation of lambdas in THF
2011-07-05, by nik
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
2011-07-05, by nik
simplified Symbol.iterator: produce strings, which are mostly preallocated;
2011-07-05, by wenzelm
tuned comment (cf. e9f26e66692d);
2011-07-05, by wenzelm
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-05, by wenzelm
theory name needs to conform to Path syntax;
2011-07-05, by wenzelm
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
2011-07-05, by wenzelm
prefer space_explode/split_lines as in Isabelle/ML;
2011-07-05, by wenzelm
Path.split convenience;
2011-07-05, by wenzelm
get theory from last executation state;
2011-07-05, by wenzelm
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
2011-07-05, by wenzelm
clarified cancel_execution/await_cancellation;
2011-07-05, by wenzelm
tuned signature;
2011-07-05, by wenzelm
tuned;
2011-07-05, by wenzelm
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
2011-07-05, by krauss
Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-07-04, by wenzelm
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
2011-07-04, by wenzelm
explicit class Counter;
2011-07-04, by wenzelm
merged
2011-07-04, by wenzelm
the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
2011-07-04, by hoelzl
equalities of subsets of atLeastLessThan
2011-07-04, by hoelzl
adding documentation of the value antiquotation to the code generation manual
2011-07-03, by bulwahn
make SML/NJ happy
2011-07-03, by blanchet
install case certificate for If after code_datatype declaration for bool
2011-07-02, by haftmann
tuned typo
2011-07-02, by haftmann
pervasive Basic_Library in Scala;
2011-07-04, by wenzelm
some support for theory files within Isabelle/Scala session;
2011-07-04, by wenzelm
imitate exception ERROR of Isabelle/ML;
2011-07-04, by wenzelm
eliminated null;
2011-07-03, by wenzelm
more explicit edit_node vs. init_node;
2011-07-03, by wenzelm
tuned signature;
2011-07-03, by wenzelm
Thy_Header.read convenience;
2011-07-02, by wenzelm
some support for Session.File_Store;
2011-07-02, by wenzelm
tuned signature;
2011-07-02, by wenzelm
eliminated redundant session_ready;
2011-07-02, by wenzelm
tuned;
2011-07-02, by wenzelm
uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;
2011-07-02, by wenzelm
misc tuning;
2011-07-02, by wenzelm
correction: do not assume that case const index covered all cases
2011-07-02, by haftmann
remove illegal case combinators after merge
2011-07-01, by haftmann
corrected misunderstanding what `old functions` are supposed to be
2011-07-01, by haftmann
centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
2011-07-01, by haftmann
merged
2011-07-01, by haftmann
index cases for constructors
2011-07-01, by haftmann
cover induct's "arbitrary" more deeply
2011-07-01, by noschinl
merged;
2011-07-01, by wenzelm
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
2011-07-01, by blanchet
made minimizer informative output accurate
2011-07-01, by blanchet
test a few more type encodings
2011-07-01, by blanchet
further repair "mangled_tags", now that tags are also mangled
2011-07-01, by blanchet
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
2011-07-01, by blanchet
renamed "type_sys" to "type_enc", which is more accurate
2011-07-01, by blanchet
document "simple_higher" type encoding
2011-07-01, by blanchet
cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
2011-07-01, by blanchet
mangle "ti" tags
2011-07-01, by blanchet
tuning
2011-07-01, by blanchet
clarified Thy_Syntax.element;
2011-07-01, by wenzelm
tuned layout;
2011-07-01, by wenzelm
proper @{binding} antiquotations (relevant for formal references);
2011-07-01, by wenzelm
tuned;
2011-07-01, by wenzelm
merged
2011-07-01, by wenzelm
reverted 782991e4180d: fold_fields was never used
2011-07-01, by noschinl
reverted ce00462f,b3759dce, 7a165592: unwanted generalisation
2011-07-01, by noschinl
improving actual dependencies
2011-07-01, by bulwahn
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
2011-07-01, by bulwahn
adding a value antiquotation
2011-07-01, by bulwahn
more general theory header parsing;
2011-06-30, by wenzelm
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
2011-06-30, by wenzelm
merged
2011-06-30, by wenzelm
parse term in auxiliary context augmented with variable;
2011-06-30, by krauss
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
2011-06-29, by boehmes
prefer Isabelle path algebra;
2011-06-30, by wenzelm
proper fold order;
2011-06-30, by wenzelm
more Path operations;
2011-06-30, by wenzelm
getenv_strict in ML;
2011-06-30, by wenzelm
standardized use of Path operations;
2011-06-30, by wenzelm
tuned comments;
2011-06-30, by wenzelm
abstract algebra of file paths in Scala (cf. path.ML);
2011-06-30, by wenzelm
proper Path.print;
2011-06-30, by wenzelm
basic operations on lists and strings;
2011-06-29, by wenzelm
tuned signature;
2011-06-29, by wenzelm
simplified/unified Simplifier.mk_solver;
2011-06-29, by wenzelm
modernized some simproc setup;
2011-06-29, by wenzelm
modernized some simproc setup;
2011-06-29, by wenzelm
print Path.T with some markup;
2011-06-29, by wenzelm
HTML: render control symbols more like Isabelle/Scala/jEdit;
2011-06-29, by wenzelm
collapse map functions with identity subcoercions to identities;
2011-06-28, by traytel
reenabled accidentally-disabled automatic minimization
2011-06-28, by blanchet
tuned markup;
2011-06-28, by wenzelm
merged
2011-06-28, by paulson
tidied messy proofs
2011-06-28, by paulson
merged
2011-06-28, by bulwahn
adding timeout to quickcheck narrowing
2011-06-28, by bulwahn
simplified proofs using metis calls
2011-06-28, by paulson
merged
2011-06-28, by paulson
keyfree: The set of key-free messages (and associated theorems)
2011-06-28, by paulson
merged
2011-06-27, by wenzelm
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
2011-06-27, by krauss
added reference for MESON
2011-06-27, by blanchet
document "meson" and "metis" in HOL specific section of the Isar ref manual
2011-06-27, by blanchet
clarify minimizer output
2011-06-27, by blanchet
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
2011-06-27, by blanchet
tweaked comment
2011-06-27, by blanchet
document "sound" option
2011-06-27, by blanchet
minor Sledgehammer news
2011-06-27, by blanchet
added "sound" option to force Sledgehammer to be pedantically sound
2011-06-27, by blanchet
removed "full_types" option from documentation
2011-06-27, by blanchet
document changes to Sledgehammer and "try"
2011-06-27, by blanchet
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
2011-06-27, by blanchet
clarify warning message to avoid confusing beginners
2011-06-27, by blanchet
remove experimental trimming feature -- it slowed down things on Linux for some reason
2011-06-27, by blanchet
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
2011-06-27, by blanchet
NEWS;
2011-06-27, by wenzelm
document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27, by wenzelm
proper checking of @{ML_antiquotation};
2011-06-27, by wenzelm
hide rather short auxiliary names, which can easily occur in user theories;
2011-06-27, by wenzelm
updated generated file;
2011-06-27, by wenzelm
ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27, by wenzelm
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-27, by wenzelm
parallel Syntax.parse, which is rather slow;
2011-06-27, by wenzelm
markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
2011-06-27, by wenzelm
move conditional expectation to its own theory file
2011-06-27, by hoelzl
updated SMT certificates
2011-06-26, by boehmes
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
2011-06-26, by boehmes
proper tokens only if session is ready;
2011-06-25, by wenzelm
entity markup for "type", "constant";
2011-06-25, by wenzelm
clarified Markup.CLASS vs. HTML.CLASS;
2011-06-25, by wenzelm
tuned color, to avoid confusion with type variables;
2011-06-25, by wenzelm
discontinued generic XML markup -- this is for XHTML with <span/> elements;
2011-06-25, by wenzelm
type classes: entity markup instead of old-style token markup;
2011-06-25, by wenzelm
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-06-25, by wenzelm
clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
2011-06-25, by wenzelm
produce string constant directly;
2011-06-25, by wenzelm
merged
2011-06-25, by wenzelm
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
2011-06-25, by ballarin
removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;
2011-06-25, by wenzelm
clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);
2011-06-25, by wenzelm
CLASSPATH already converted in isabelle java wrapper;
2011-06-25, by wenzelm
removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
2011-06-25, by wenzelm
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
2011-06-23, by wenzelm
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
2011-06-23, by wenzelm
more robust concurrent builds;
2011-06-23, by wenzelm
merged
2011-06-23, by huffman
add countable_datatype method for proving countable class instances
2011-06-23, by huffman
merged;
2011-06-23, by wenzelm
instance inat :: number_semiring
2011-06-23, by huffman
added number_semiring class, plus a few new lemmas;
2011-06-23, by huffman
merged
2011-06-23, by blanchet
fiddle with remote ATP settings, based on Judgment Day
2011-06-23, by blanchet
give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers
2011-06-23, by blanchet
Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
2011-06-23, by ballarin
generalize lemmas power_number_of_even and power_number_of_odd
2011-06-22, by huffman
merged
2011-06-22, by huffman
add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
2011-06-22, by huffman
simplified arrangement of jars;
2011-06-23, by wenzelm
adapted to Cygwin;
2011-06-23, by wenzelm
provide Isabelle/Scala environment as Java extension, instead of user classpath
2011-06-23, by wenzelm
explicit import java.lang.System to prevent odd scope problems;
2011-06-23, by wenzelm
ensure export of initial CLASSPATH;
2011-06-23, by wenzelm
augment Java extension directories;
2011-06-23, by wenzelm
basic setup for Isabelle charset;
2011-06-23, by wenzelm
prefer actual charset over charset name;
2011-06-22, by wenzelm
clarified default ML settings;
2011-06-22, by wenzelm
lazy Isabelle_System.default supports implicit boot;
2011-06-22, by wenzelm
clarified plugin start/stop;
2011-06-22, by wenzelm
clarified init/exit procedure;
2011-06-22, by wenzelm
clarified decoded control symbols;
2011-06-22, by wenzelm
init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
2011-06-22, by wenzelm
prefer STIXGeneral -- hard to tell if better or worse;
2011-06-22, by wenzelm
merged
2011-06-22, by wenzelm
export lambda-lifting code as there is potential use for it within Sledgehammer
2011-06-22, by boehmes
updated to jedit-4.4.1 and jedit_build-20110622;
2011-06-22, by wenzelm
clarified chunk.offset, chunk.length;
2011-06-22, by wenzelm
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
2011-06-21, by wenzelm
some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;
2011-06-21, by wenzelm
more precise font transformations: shift sub/superscript, adjust size for user fonts;
2011-06-21, by wenzelm
don't change the way helpers are generated for the exporter's sake
2011-06-21, by blanchet
provide appropriate type system and number of fact defaults for remote ATPs
2011-06-21, by blanchet
order generated facts topologically
2011-06-21, by blanchet
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
2011-06-21, by blanchet
tweaked E, SPASS, Vampire setup based on latest Judgment Day results
2011-06-21, by blanchet
remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
2011-06-21, by blanchet
avoid double ASCII-fication
2011-06-21, by blanchet
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
2011-06-21, by blanchet
generate type predicates for existentials/skolems, otherwise some problems might not be provable
2011-06-21, by blanchet
insert rather than append special facts to make it less likely that they're truncated away
2011-06-21, by blanchet
hidden font: full height makes cursor more visible;
2011-06-21, by wenzelm
more uniform treatment of recode_set/recode_map;
2011-06-21, by wenzelm
tuned iteration over short symbols;
2011-06-21, by wenzelm
Symbol.is_ctrl: handle decoded version as well;
2011-06-21, by wenzelm
some support for user symbol fonts;
2011-06-21, by wenzelm
removed obsolete font specification;
2011-06-20, by wenzelm
more tolerant Symbol.decode;
2011-06-20, by wenzelm
simplified/generalized ISABELLE_FONTS handling;
2011-06-20, by wenzelm
updated to jedit_build-20110620;
2011-06-20, by wenzelm
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
2011-06-20, by wenzelm
clean up SPASS FLOTTER hack
2011-06-20, by blanchet
remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers
2011-06-20, by blanchet
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
2011-06-20, by blanchet
slightly better setup for E
2011-06-20, by blanchet
respect "really_all" argument, which is used by "ATP_Export"
2011-06-20, by blanchet
slightly better setup for SPASS and Vampire as more results have come in
2011-06-20, by blanchet
optimized SPASS and Vampire time slices, like E before
2011-06-20, by blanchet
optimized E's time slicing, based on latest exhaustive Judgment Day results
2011-06-20, by blanchet
deal with ATP time slices in a more flexible/robust fashion
2011-06-20, by blanchet
literal unicode in README.html allows to copy/paste from Lobo output;
2011-06-20, by wenzelm
merged;
2011-06-19, by wenzelm
explain special control symbols;
2011-06-19, by wenzelm
accept control symbols;
2011-06-19, by wenzelm
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
2011-06-19, by blanchet
recognize one more E failure message
2011-06-19, by blanchet
tweaked TPTP formula kind for typing information used in the conjecture
2011-06-19, by blanchet
more forceful message
2011-06-19, by blanchet
treat quotes as non-controllable, to reduce surprise in incremental editing;
2011-06-19, by wenzelm
abbreviations for special control symbols;
2011-06-19, by wenzelm
completion for control symbols;
2011-06-19, by wenzelm
updated to jedit_build-20110619;
2011-06-19, by wenzelm
support for bold style within text buffer;
2011-06-19, by wenzelm
tuned;
2011-06-19, by wenzelm
discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);
2011-06-19, by wenzelm
added glyphs 21e0..21e4, 21e6..21e9, 2759 from DejaVuSansMono;
2011-06-19, by wenzelm
names for control symbols without "^", which is relevant for completion;
2011-06-19, by wenzelm
some unicode chars for special control symbols;
2011-06-19, by wenzelm
tuned;
2011-06-19, by wenzelm
tuned markup;
2011-06-18, by wenzelm
avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
2011-06-18, by wenzelm
proper gfx.setColor;
2011-06-18, by wenzelm
proper x1;
2011-06-18, by wenzelm
convenience functions;
2011-06-18, by wenzelm
more robust caret painting wrt. surrogate characters;
2011-06-18, by wenzelm
do not control malformed symbols;
2011-06-18, by wenzelm
Buffer.editSyntaxStyle: mask extended syntax styles;
2011-06-18, by wenzelm
hardwired abbreviations for standard control symbols;
2011-06-18, by wenzelm
updated to jedit_build-20110618, which is required for sub/superscript rendering;
2011-06-18, by wenzelm
basic support for extended syntax styles: sub/superscript;
2011-06-18, by wenzelm
tuned -- Map.empty serves as partial function;
2011-06-18, by wenzelm
proper place for config files (cf. 55866987a7d9);
2011-06-18, by wenzelm
tuned signature;
2011-06-18, by wenzelm
merged
2011-06-18, by wenzelm
IMP compiler with int, added reverse soundness direction
2011-06-17, by kleing
proper place for config files;
2011-06-18, by wenzelm
tuned markup;
2011-06-18, by wenzelm
highlight via foreground painter, using alpha channel;
2011-06-18, by wenzelm
tuned signature;
2011-06-18, by wenzelm
tuned text;
2011-06-18, by wenzelm
inner literal/delimiter corresponds to outer keyword/operator;
2011-06-18, by wenzelm
tuned markup;
2011-06-18, by wenzelm
more uniform treatment of "keyword" vs. "operator";
2011-06-18, by wenzelm
simplified Line_Context (again);
2011-06-18, by wenzelm
more robust treatment of partial range restriction;
2011-06-18, by wenzelm
select_markup: no filtering here -- results may be distorted anyway;
2011-06-18, by wenzelm
more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;
2011-06-17, by wenzelm
more explicit error message;
2011-06-17, by wenzelm
merged
2011-06-17, by wenzelm
gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
2011-06-16, by blanchet
added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users
2011-06-16, by blanchet
fixed soundness bug related to extensionality
2011-06-16, by blanchet
less
more
|
(0)
-30000
-10000
-1920
+1920
+10000
+30000
tip