Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf);
2010-11-28, by wenzelm
removed HOLCF for now as explicit component
2010-11-28, by krauss
fix cut-and-paste errors for HOLCF entries in IsaMakefile
2010-11-27, by huffman
update web description of HOLCF;
2010-11-27, by huffman
remove HOLCF from build script, since it no longer works
2010-11-27, by huffman
moved directory src/HOLCF to src/HOL/HOLCF;
2010-11-27, by huffman
merged
2010-11-27, by huffman
rename Pcpodef.thy to Cpodef.thy;
2010-11-27, by huffman
renamed several HOLCF theorems (listed in NEWS)
2010-11-27, by huffman
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
2010-11-27, by huffman
rename rep_contlub lemmas to rep_lub
2010-11-27, by huffman
rename function 'match_UU' to 'match_bottom'
2010-11-27, by huffman
rename function 'strict' to 'seq', which is its name in Haskell
2010-11-27, by huffman
merged
2010-11-27, by haftmann
merged
2010-11-27, by haftmann
typscheme with signatures is inappropriate when building empty certificate;
2010-11-27, by haftmann
merged
2010-11-27, by haftmann
merged
2010-11-27, by haftmann
corrected: use canonical variables of type scheme uniformly
2010-11-27, by haftmann
tuned
2010-11-27, by haftmann
merged
2010-11-26, by haftmann
consider sort constraints for datatype constructors when constructing the empty equation certificate;
2010-11-26, by haftmann
tuned example
2010-11-26, by haftmann
merged
2010-11-27, by wenzelm
updated generated documents
2010-11-27, by haftmann
added equation for Queue;
2010-11-27, by haftmann
added evaluation section
2010-11-27, by haftmann
tuned formatting;
2010-11-27, by haftmann
added label
2010-11-27, by haftmann
more thorough process termination (cf. Scala version);
2010-11-27, by wenzelm
prefer Isabelle/ML concurrency elements;
2010-11-27, by wenzelm
removed bash from ML system bootstrap, and past the Secure ML barrier;
2010-11-27, by wenzelm
more proper int wrappers;
2010-11-27, by wenzelm
explicit check for requirement;
2010-11-27, by wenzelm
more basic Isabelle_System.mkdir;
2010-11-27, by wenzelm
tuned;
2010-11-27, by wenzelm
more explicit Isabelle_System operations;
2010-11-27, by wenzelm
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
2010-11-27, by wenzelm
moved file identification to thy_load.ML (where it is actually used);
2010-11-27, by wenzelm
removed some old settings;
2010-11-27, by wenzelm
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
2010-11-27, by wenzelm
merged
2010-11-26, by huffman
remove map function names from domain package theory data
2010-11-26, by huffman
isar-style proof for lemma contI2
2010-11-26, by huffman
remove case combinator for fixrec match type
2010-11-26, by huffman
declare more simp rules for powerdomains
2010-11-26, by huffman
merged;
2010-11-27, by wenzelm
merged
2010-11-26, by haftmann
strict forall2
2010-11-26, by haftmann
nbe decides equality of abstractions by extensionality
2010-11-26, by haftmann
eliminated some generated comments;
2010-11-26, by wenzelm
merged
2010-11-26, by wenzelm
merged
2010-11-26, by haftmann
keep type variable arguments of datatype constructors in bookkeeping
2010-11-26, by haftmann
document changes in Nitpick and MESON/Metis
2010-11-26, by blanchet
renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first
2010-11-26, by blanchet
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
2010-11-26, by blanchet
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-26, by wenzelm
just one version of fold_rev2;
2010-11-26, by wenzelm
explicit use of unprefix;
2010-11-26, by wenzelm
keep private things private, without comments;
2010-11-26, by wenzelm
eliminated some clones of eq_list;
2010-11-26, by wenzelm
merged
2010-11-26, by nipkow
new lemma
2010-11-26, by nipkow
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
2010-11-26, by wenzelm
prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
2010-11-26, by wenzelm
discontinued global "Isabelle" symlink, to make each distribution even more self-contained;
2010-11-26, by wenzelm
more correct spelling;
2010-11-26, by wenzelm
globbing constant expressions use more idiomatic underscore rather than star
2010-11-26, by haftmann
globbing constant expressions use more idiomatic underscore rather than star;
2010-11-26, by haftmann
datatype constructor glob for code_reflect
2010-11-26, by haftmann
merged
2010-11-26, by haftmann
merged
2010-11-26, by haftmann
merged
2010-11-25, by haftmann
toplevel deresolving for flat module name space
2010-11-25, by haftmann
merged
2010-11-26, by hoelzl
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-11-23, by hoelzl
Replace surj by abbreviation; remove surj_on.
2010-11-22, by hoelzl
adjust Sledgehammer/SMT fudge factor
2010-11-26, by blanchet
clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies);
2010-11-25, by wenzelm
merge
2010-11-25, by blanchet
cosmetics
2010-11-25, by blanchet
eta-reduce on the fly to prevent an exception
2010-11-25, by blanchet
merged
2010-11-25, by nipkow
Added the simplest finite Ramsey theorem
2010-11-25, by nipkow
reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions
2010-11-25, by blanchet
set Metis option on correct context, lest it be ignored
2010-11-25, by blanchet
make "debug" mode of Sledgehammer/SMT more liberal
2010-11-25, by blanchet
fix check for builtinness of 0 and 1 -- these aren't functions
2010-11-25, by blanchet
added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway
2010-11-25, by blanchet
document requirement on theory import
2010-11-24, by blanchet
corrected abd4e7358847 where SOMEthing went utterly wrong
2010-11-24, by haftmann
merged
2010-11-24, by boehmes
swap names for built-in tester functions (to better reflect the intuition of what they do);
2010-11-24, by boehmes
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
2010-11-24, by boehmes
more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers
2010-11-24, by blanchet
removing Enum.in_enum from the claset
2010-11-24, by bulwahn
merged
2010-11-24, by boehmes
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
2010-11-24, by boehmes
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
2010-11-24, by boehmes
announcing some latest change (d40b347d5b0b)
2010-11-24, by bulwahn
merged
2010-11-23, by blanchet
more precise characterization of built-in constants "number_of", "0", and "1"
2010-11-23, by blanchet
merged
2010-11-23, by haftmann
merged
2010-11-22, by haftmann
adhere established Collect/mem convention more closely
2010-11-22, by haftmann
merged
2010-11-22, by haftmann
replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-22, by haftmann
renamed slightly ambivalent crel to effect
2010-11-22, by haftmann
disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day
2010-11-23, by blanchet
more precise error handling for Z3;
2010-11-23, by blanchet
use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on
2010-11-23, by blanchet
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
2010-11-23, by blanchet
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
2010-11-23, by blanchet
added "verbose" option to Metis to shut up its warnings if necessary
2010-11-23, by blanchet
added support for quantifier weight annotations
2010-11-22, by boehmes
share and use more utility functions;
2010-11-22, by boehmes
added prove reconstruction for injective functions;
2010-11-22, by boehmes
generous timeout gives more breath in parallel run on less luxury machines
2010-11-22, by haftmann
adding setup for exhaustive testing in example file
2010-11-22, by bulwahn
hiding enum
2010-11-22, by bulwahn
adapting example in Predicate_Compile_Examples
2010-11-22, by bulwahn
hiding the constants
2010-11-22, by bulwahn
improving function is_iterable in quickcheck
2010-11-22, by bulwahn
adding temporary options to the quickcheck examples
2010-11-22, by bulwahn
adapting the quickcheck examples
2010-11-22, by bulwahn
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
2010-11-22, by bulwahn
adding code equations for EX1 on finite types
2010-11-22, by bulwahn
adding code equation for function equality; adding some instantiations for the finite types
2010-11-22, by bulwahn
adding Enum to HOL-Main image and removing it from HOL-Library
2010-11-22, by bulwahn
moving Enum theory from HOL/Library to HOL
2010-11-22, by bulwahn
splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
2010-11-22, by bulwahn
adding prototype for finite_type instantiations
2010-11-22, by bulwahn
adding option finite_types to quickcheck
2010-11-22, by bulwahn
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
2010-11-22, by bulwahn
changed old-style quickcheck configurations to new Config.T configurations
2010-11-22, by bulwahn
adding temporary function test_test_small to Quickcheck
2010-11-22, by bulwahn
added useful function map_context_result to signature
2010-11-22, by bulwahn
moving the error handling to the right scope in smallvalue_generators
2010-11-22, by bulwahn
removing clone from function package and using the clean interface from Function_Relation instead
2010-11-22, by bulwahn
adding function generation to SmallCheck; activating exhaustive search space testing
2010-11-22, by bulwahn
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
2010-11-22, by bulwahn
generalized ensure_random_datatype to ensure_sort_datatype
2010-11-22, by bulwahn
renaming quickcheck generator code to random
2010-11-22, by bulwahn
ported sledgehammer_tactic to current development version
2010-11-22, by bulwahn
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
2010-11-22, by bulwahn
adding files to use sledgehammer as a tactic for non-interactive use
2010-11-22, by bulwahn
adding birthday paradoxon from some abandoned drawer
2010-11-22, by bulwahn
adding extensional function spaces to the FuncSet library theory
2010-11-22, by bulwahn
tuned
2010-11-22, by haftmann
tuned
2010-11-22, by haftmann
updated explode vs. raw_explode;
2010-11-20, by wenzelm
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-20, by wenzelm
total Symbol.explode (cf. 1050315f6ee2);
2010-11-19, by wenzelm
do not export Thy_Load.required, to avoid confusion about the interface;
2010-11-19, by wenzelm
merged
2010-11-19, by huffman
declare adm_chfin [simp]
2010-11-17, by huffman
add lemma cont_fun; remove unused lemma monofun_app
2010-11-17, by huffman
accumulated NEWS updates for HOLCF
2010-11-17, by huffman
section -> subsection
2010-11-17, by huffman
add lemma adm_prod_case
2010-11-17, by huffman
merged
2010-11-19, by paulson
First-order pattern matching: catch a rogue exception (differing numbers of arguments)
2010-11-19, by paulson
eval simp rules for predicate type, simplify primitive proofs
2010-11-19, by haftmann
generalized type
2010-11-19, by haftmann
made smlnj happy
2010-11-19, by haftmann
merged
2010-11-19, by haftmann
proper qualification needed due to shadowing on theory merge
2010-11-18, by haftmann
more appropriate name for property
2010-11-18, by haftmann
mapper for sum type
2010-11-18, by haftmann
mapper for option type
2010-11-18, by haftmann
mapper for list type; map_pair replaces prod_fun
2010-11-18, by haftmann
map_pair replaces prod_fun
2010-11-18, by haftmann
mapper for mulitset type
2010-11-18, by haftmann
mapper for mapping type
2010-11-18, by haftmann
mapper for fset type
2010-11-18, by haftmann
mapper for dlist type
2010-11-18, by haftmann
map_fun combinator in theory Fun
2010-11-18, by haftmann
some updates after 2 years of Mercurial usage;
2010-11-18, by wenzelm
mention Sledgehammer with SMT
2010-11-18, by blanchet
enabled SMT solver in Sledgehammer by default
2010-11-18, by blanchet
merged
2010-11-18, by haftmann
keep variables bound
2010-11-18, by haftmann
remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
2010-11-18, by blanchet
merged
2010-11-17, by haftmann
infer variances of user-given mapper operation; proper thm storing
2010-11-17, by haftmann
code eqn for slice was missing; redefined splice with fun
2010-11-17, by nipkow
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
2010-11-17, by huffman
merged
2010-11-17, by huffman
typedef (open) unit
2010-11-16, by huffman
add bind_bind rules for powerdomains
2010-11-16, by huffman
merged
2010-11-17, by wenzelm
emerging Isar command interface
2010-11-17, by haftmann
fixed typo
2010-11-17, by haftmann
updated keywords
2010-11-17, by haftmann
ML signature interface
2010-11-17, by haftmann
stub for Isar command interface
2010-11-17, by haftmann
module for functorial mappers
2010-11-17, by haftmann
merged
2010-11-17, by wenzelm
require the b2i file ending in the boogie_open command (for consistency with the theory header)
2010-11-17, by boehmes
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
2010-11-17, by boehmes
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
2010-11-17, by boehmes
add lemmas about powerdomains
2010-11-16, by huffman
declare {upper,lower,convex}_pd_induct as default induction rules
2010-11-16, by huffman
rename 'repdef' to 'domaindef'
2010-11-16, by huffman
refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
2010-11-17, by wenzelm
less parentheses, cf. Session.welcome;
2010-11-17, by wenzelm
avoid spam;
2010-11-16, by wenzelm
more robust determination of java executable;
2010-11-16, by wenzelm
init_component: require absolute path (when invoked by user scripts);
2010-11-16, by wenzelm
more explicit explanation of init_component shell function;
2010-11-16, by wenzelm
paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
2010-11-16, by wenzelm
tuned message;
2010-11-16, by wenzelm
post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);
2010-11-16, by wenzelm
more reasonably defaults for typical laptops (2 GB RAM, 2 cores);
2010-11-16, by wenzelm
added forall2 predicate lifter
2010-11-16, by haftmann
merged
2010-11-15, by wenzelm
merged
2010-11-15, by boehmes
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
2010-11-15, by boehmes
honour timeouts which are not rounded to full seconds
2010-11-15, by boehmes
better error message
2010-11-15, by blanchet
better error message
2010-11-15, by blanchet
merged
2010-11-15, by wenzelm
cosmetics
2010-11-15, by blanchet
interpret SMT_Failure.Solver_Crashed correctly
2010-11-15, by blanchet
turn on Sledgehammer verbosity so we can track down crashes
2010-11-15, by blanchet
pick up SMT solver crashes and report them to the user/Mirabelle if desired
2010-11-15, by blanchet
merged
2010-11-15, by boehmes
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
2010-11-15, by boehmes
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
2010-11-15, by boehmes
merged
2010-11-15, by bulwahn
ignoring the constant STR in the predicate compiler
2010-11-15, by bulwahn
non-executable source files;
2010-11-15, by wenzelm
eliminated old-style sed in favour of builtin regex matching;
2010-11-15, by wenzelm
more robust treatment of spaces in file names;
2010-11-15, by wenzelm
tuned error messages;
2010-11-15, by wenzelm
merged
2010-11-15, by wenzelm
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
re-generalized type of prod_rel (accident from 2989f9f3aa10)
2010-11-15, by haftmann
formal dependency on b2i files
2010-11-15, by boehmes
merged
2010-11-14, by boehmes
check the return code of the SMT solver and raise an exception if the prover failed
2010-11-12, by boehmes
updated README;
2010-11-14, by wenzelm
tuned;
2010-11-14, by wenzelm
cover 'write' as primitive proof command;
2010-11-14, by wenzelm
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
2010-11-14, by wenzelm
somewhat adhoc replacement for 'thus' and 'hence';
2010-11-13, by wenzelm
always print state of proof commands (notably "qed" etc.);
2010-11-13, by wenzelm
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
2010-11-13, by wenzelm
tuned message;
2010-11-13, by wenzelm
proper escape in regex;
2010-11-13, by wenzelm
report malformed symbols;
2010-11-13, by wenzelm
qualified Symbol_Pos.symbol;
2010-11-13, by wenzelm
total Symbol.source;
2010-11-13, by wenzelm
eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-11-13, by wenzelm
treat Unicode "replacement character" (i.e. decoding error) is malformed;
2010-11-13, by wenzelm
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
2010-11-13, by wenzelm
tuned;
2010-11-13, by wenzelm
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
2010-11-13, by wenzelm
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
2010-11-13, by wenzelm
updated README;
2010-11-13, by wenzelm
defensive defaults for more robust experience for new users;
2010-11-12, by wenzelm
merged
2010-11-12, by wenzelm
preliminary support for newer versions of Z3
2010-11-12, by boehmes
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
2010-11-12, by boehmes
let the theory formally depend on the Boogie output
2010-11-12, by boehmes
look for certificates relative to the theory
2010-11-12, by boehmes
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
2010-11-12, by boehmes
merged
2010-11-12, by huffman
update Theory.requires with new theory name
2010-11-12, by huffman
tuned signatures;
2010-11-12, by wenzelm
never open Unsynchronized;
2010-11-12, by wenzelm
merged
2010-11-12, by wenzelm
section headings
2010-11-10, by huffman
reorder chapters for generated document
2010-11-10, by huffman
merge Representable.thy into Domain.thy
2010-11-10, by huffman
move stuff from Domain.thy to Domain_Aux.thy
2010-11-10, by huffman
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-11-10, by huffman
allow unpointed lazy arguments for definitional domain package
2010-11-10, by huffman
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
2010-11-10, by huffman
merged
2010-11-10, by huffman
removed unused lemma chain_mono2
2010-11-10, by huffman
rename class 'bifinite' to 'domain'
2010-11-10, by huffman
instance sum :: (predomain, predomain) predomain
2010-11-10, by huffman
configure sum type for fixrec
2010-11-10, by huffman
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
2010-11-10, by huffman
instance prod :: (predomain, predomain) predomain
2010-11-10, by huffman
adapt isodefl proof script to unpointed types
2010-11-09, by huffman
add 'predomain' class: unpointed version of bifinite
2010-11-09, by huffman
add bifiniteness check for domain_isomorphism command
2010-11-09, by huffman
implement map_of_typ using Pattern.rewrite_term
2010-11-09, by huffman
avoid using stale theory
2010-11-09, by huffman
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
2010-11-08, by huffman
add function the_sort
2010-11-08, by huffman
refactor tmp_thy code
2010-11-08, by huffman
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
2010-11-08, by huffman
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
2010-11-12, by wenzelm
Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
2010-11-12, by wenzelm
more precise treatment of deleted nodes;
2010-11-11, by wenzelm
tuned error message;
2010-11-11, by wenzelm
unified type Document.Edit;
2010-11-11, by wenzelm
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
2010-11-11, by wenzelm
tuned;
2010-11-11, by wenzelm
reduced danger of line breaks within minipage;
2010-11-11, by wenzelm
Sidekick block asset: show first line only;
2010-11-10, by wenzelm
added buffer_text convenience, with explicit locking;
2010-11-10, by wenzelm
use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);
2010-11-10, by wenzelm
merged
2010-11-10, by wenzelm
make SML/NJ happy
2010-11-10, by blanchet
merged
2010-11-09, by haftmann
slightly changed fun_map_def
2010-11-09, by haftmann
fun_rel_def is no simp rule by default
2010-11-09, by haftmann
more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
2010-11-09, by haftmann
more appropriate specification packages; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
type annotations in specifications; fun_rel_def is no simp rule by default
2010-11-09, by haftmann
fun_rel_def is no simp rule by default
2010-11-09, by haftmann
merged
2010-11-09, by paulson
tidied using metis
2010-11-09, by paulson
manage folding via sidekick by default;
2010-11-10, by wenzelm
eliminated obsolete heading category -- superseded by heading_level;
2010-11-10, by wenzelm
treat main theory commands like headings, and nest anything else inside;
2010-11-10, by wenzelm
proper treatment of equal heading level;
2010-11-10, by wenzelm
added missing Keyword.THY_SCHEMATIC_GOAL;
2010-11-10, by wenzelm
default Sidekick parser based on section headings;
2010-11-10, by wenzelm
some support for nested source structure, based on section headings;
2010-11-10, by wenzelm
tuned;
2010-11-10, by wenzelm
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
2010-11-09, by wenzelm
updated version;
2010-11-09, by wenzelm
private counter, to keep externalized ids a bit smaller;
2010-11-09, by wenzelm
added general Synchronized.counter convenience;
2010-11-09, by wenzelm
explicitly identify forked/joined tasks;
2010-11-09, by wenzelm
accomodate old manuals that include pdfsetup.sty without isabelle.sty;
2010-11-09, by wenzelm
merged
2010-11-09, by wenzelm
removed type-inference-like behaviour from relation_tac completely; tuned
2010-11-08, by krauss
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
2010-11-08, by wenzelm
explicitly check uniqueness of symbol recoding;
2010-11-08, by wenzelm
more hints on building and running Isabelle/jEdit from command line;
2010-11-08, by wenzelm
merged
2010-11-08, by wenzelm
merge
2010-11-08, by blanchet
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
2010-11-08, by blanchet
merged
2010-11-08, by huffman
merged
2010-11-06, by huffman
(infixl "<<" 55) -> (infix "<<" 50)
2010-11-05, by huffman
simplify some proofs
2010-11-03, by huffman
remove unnecessary stuff from Discrete.thy
2010-11-03, by huffman
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-11-03, by huffman
add lemma eq_imp_below
2010-11-03, by huffman
discontinue a bunch of legacy theorem names
2010-11-03, by huffman
move a few admissibility lemmas into FOCUS/Stream_adm.thy
2010-11-03, by huffman
simplify some proofs
2010-11-03, by huffman
compile -- 7550b2cba1cb broke the build
2010-11-08, by blanchet
merge
2010-11-08, by blanchet
recognize Vampire error
2010-11-08, by blanchet
return the process return code along with the process outputs
2010-11-08, by boehmes
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-08, by boehmes
merged
2010-11-08, by haftmann
corrected slip: must keep constant map, not type map; tuned code
2010-11-08, by haftmann
constructors to datatypes in code_reflect can be globbed; dropped unused code
2010-11-08, by haftmann
adding code and theory for smallvalue generators, but do not setup the interpretation yet
2010-11-08, by bulwahn
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
2010-11-08, by blanchet
better detection of completely irrelevant facts
2010-11-08, by blanchet
always use a hard timeout in Mirabelle
2010-11-07, by blanchet
use "smt" (rather than "metis") to reconstruct SMT proofs
2010-11-07, by blanchet
don't pass too many facts on the first iteration of the SMT solver
2010-11-07, by blanchet
catch TimeOut exception
2010-11-07, by blanchet
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
2010-11-07, by blanchet
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
2010-11-07, by blanchet
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
2010-11-07, by blanchet
make Nitpick datatype tests faster to make timeout less likely
2010-11-06, by blanchet
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
2010-11-06, by blanchet
always honor the max relevant constraint
2010-11-06, by blanchet
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
2010-11-08, by wenzelm
updated generated files;
2010-11-08, by wenzelm
tweaked pdf setup to allow modification of \pdfminorversion;
2010-11-07, by wenzelm
merged;
2010-11-07, by wenzelm
updated generated files;
2010-11-07, by wenzelm
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
2010-11-07, by wenzelm
updated generated file;
2010-11-07, by wenzelm
more literal appearance of antiqopen/antiqclose;
2010-11-07, by wenzelm
'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
2010-11-07, by wenzelm
continue after failed commands;
2010-11-06, by wenzelm
added Keyword.is_heading (cf. Scala version);
2010-11-06, by wenzelm
updated keywords;
2010-11-06, by wenzelm
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-11-06, by wenzelm
somewhat more uniform timing markup in ML vs. Scala;
2010-11-06, by wenzelm
somewhat more uniform timing in ML vs. Scala;
2010-11-06, by wenzelm
added Markup.Double, Markup.Double_Property;
2010-11-06, by wenzelm
explicit "timing" status for toplevel transactions;
2010-11-06, by wenzelm
tuned;
2010-11-06, by wenzelm
tuned comments;
2010-11-06, by wenzelm
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-11-06, by krauss
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
2010-11-05, by wenzelm
updated keywords;
2010-11-05, by wenzelm
reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;
2010-11-05, by wenzelm
eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline;
2010-11-05, by wenzelm
reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;
2010-11-05, by wenzelm
obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);
2010-11-05, by wenzelm
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-05, by wenzelm
updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
2010-11-05, by wenzelm
proper spelling;
2010-11-05, by wenzelm
merged
2010-11-05, by hoelzl
Extend convex analysis by Bogdan Grechuk
2010-11-05, by hoelzl
merged
2010-11-05, by blanchet
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-05, by blanchet
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
2010-11-05, by blanchet
pass proper type to SMT_Builtin.is_builtin
2010-11-04, by blanchet
remove " s" suffix since seconds are now implicit
2010-11-04, by blanchet
ignore facts with only theory constants in them
2010-11-04, by blanchet
cosmetics
2010-11-04, by blanchet
use the SMT integration's official list of built-ins
2010-11-04, by blanchet
added class relation group_add < cancel_semigroup_add
2010-11-05, by haftmann
merged
2010-11-05, by bulwahn
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
2010-11-05, by bulwahn
added two lemmas about injectivity of concat to the list theory
2010-11-05, by bulwahn
adding documentation of some quickcheck options
2010-11-05, by bulwahn
merged
2010-11-05, by haftmann
Code.check_const etc.: reject too specific types
2010-11-04, by haftmann
corrected quoting
2010-11-04, by haftmann
added lemma length_alloc
2010-11-04, by haftmann
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
2010-11-04, by haftmann
added note on countable types
2010-11-04, by haftmann
simulate more closely the behaviour of the tactic
2010-11-04, by boehmes
merged
2010-11-04, by wenzelm
merged
2010-11-04, by haftmann
merged
2010-11-04, by haftmann
dropped debug message
2010-11-03, by haftmann
more precise text
2010-11-03, by haftmann
SMLdummy target
2010-11-03, by haftmann
fixed typos
2010-11-03, by haftmann
moved theory Quicksort from Library/ to ex/
2010-11-03, by haftmann
Theory Multiset provides stable quicksort implementation of sort_key.
2010-11-03, by haftmann
added code lemmas for stable parametrized quicksort
2010-11-03, by haftmann
tuned proof
2010-11-03, by haftmann
moved file in makefile to reflect actual dependencies
2010-11-04, by blanchet
give E one more second, to prevent cases where it finds a proof but has no time to print it
2010-11-03, by blanchet
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
2010-11-03, by blanchet
don't be overly verbose in Sledgehammer's minimizer
2010-11-03, by blanchet
standardize on seconds for Nitpick and Sledgehammer timeouts
2010-11-03, by blanchet
cleaned up
2010-11-03, by nipkow
added property "tooltip-margin";
2010-11-04, by wenzelm
clarified tooltips: message output by default, extra info via control/command;
2010-11-04, by wenzelm
warn in correlation with report -- avoid spurious message duplicates;
2010-11-04, by wenzelm
tuned;
2010-11-04, by wenzelm
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
2010-11-03, by wenzelm
merged
2010-11-03, by boehmes
updated SMT certificates
2010-11-03, by boehmes
standardize timeout value based on reals
2010-11-03, by boehmes
merged
2010-11-03, by wenzelm
merged
2010-11-03, by huffman
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
2010-10-30, by huffman
merged
2010-10-30, by huffman
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
2010-10-29, by huffman
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
2010-10-29, by huffman
simplify proof of typedef_cont_Abs
2010-10-29, by huffman
rename constant trifte to tr_case
2010-10-27, by huffman
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
2010-10-27, by huffman
make syntax of continuous if-then-else consistent with HOL if-then-else
2010-10-27, by huffman
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
2010-10-27, by huffman
polyml_as_definition does not require explicit dependencies on external ML files
2010-11-03, by haftmann
explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
2010-11-03, by wenzelm
discontinued obsolete function sys_error and exception SYS_ERROR;
2010-11-03, by wenzelm
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03, by wenzelm
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03, by wenzelm
try_param_tac: plain user error appears more appropriate;
2010-11-03, by wenzelm
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03, by wenzelm
eliminated dead code;
2010-11-03, by wenzelm
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
2010-11-03, by wenzelm
removed assumption
2010-11-03, by nipkow
more on naming tactics;
2010-11-02, by wenzelm
merged
2010-11-02, by wenzelm
merged
2010-11-02, by haftmann
tuned proof
2010-11-02, by haftmann
tuned proof
2010-11-02, by haftmann
tuned lemma proposition of properties_for_sort_key
2010-11-02, by haftmann
lemmas sorted_map_same, sorted_same
2010-11-02, by haftmann
lemmas multiset_of_filter, sort_key_by_quicksort
2010-11-02, by haftmann
more on "Time" in Isabelle/ML;
2010-11-02, by wenzelm
simplified some time constants;
2010-11-02, by wenzelm
added convenience operation seconds: real -> time;
2010-11-02, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip