isabelle: Graph

merged
2010-12-06, by wenzelm
fix monotonicity type of None
2010-12-06, by blanchet
compile
2010-12-06, by blanchet
introduced hack to exploit the symmetry of equality in monotonicity calculus
2010-12-06, by blanchet
cleanup example
2010-12-06, by blanchet
add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
2010-12-06, by blanchet
fixed bug in monotonicity solution display, whereby the polarity of literals was ignored
2010-12-06, by blanchet
improve precision of forall in constancy part of the monotonicity calculus
2010-12-06, by blanchet
added some missing well-annotatedness constraints to monotonicity calculus
2010-12-06, by blanchet
more work on the monotonicity evaluation driver
2010-12-06, by blanchet
improve precision of finite functions in monotonicity calculus
2010-12-06, by blanchet
added ML code for testing entire theories for monotonicity
2010-12-06, by blanchet
use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus
2010-12-06, by blanchet
added examples to exercise new monotonicity code
2010-12-06, by blanchet
fixed quantifier handling of new monotonicity calculus
2010-12-06, by blanchet
tune parentheses and indentation
2010-12-06, by blanchet
proper handling of frames for connectives in monotonicity calculus
2010-12-06, by blanchet
tune indentation
2010-12-06, by blanchet
removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
2010-12-06, by blanchet
implemented All rules from new monotonicity calculus
2010-12-06, by blanchet
fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints
2010-12-06, by blanchet
started implementing the new monotonicity rules for application
2010-12-06, by blanchet
implemented connectives in new monotonicity calculus
2010-12-06, by blanchet
added "Neq" operator to monotonicity inference module
2010-12-06, by blanchet
started implementing connectives in new monotonicity calculus
2010-12-06, by blanchet
more work on frames in the new monotonicity calculus
2010-12-06, by blanchet
support 3 monotonicity calculi in one and fix soundness bug
2010-12-06, by blanchet
tuning
2010-12-06, by blanchet
proper handling of assignment disjunctions vs. conjunctions
2010-12-06, by blanchet
adapt monotonicity code to four annotation types
2010-12-06, by blanchet
more monotonicity tuning
2010-12-06, by blanchet
tuning
2010-12-06, by blanchet
added frame component to Gamma in monotonicity calculus
2010-12-06, by blanchet
use boolean pair to encode annotation, which may now take four values
2010-12-06, by blanchet
started generalizing monotonicity code to accommodate new calculus
2010-12-06, by blanchet
merged
2010-12-06, by blanchet
handle "max_relevant" uniformly
2010-12-06, by blanchet
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
2010-12-06, by blanchet
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
2010-12-06, by blanchet
return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
2010-12-06, by blanchet
trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
2010-12-06, by blanchet
reraise interrupt exceptions
2010-12-06, by blanchet
[mq]: sledge_binary_minimizer
2010-12-06, by blanchet
correcting usage documentation in mirabelle tool
2010-12-06, by bulwahn
adding mutabelle as a component and an isabelle tool to be used in regression testing
2010-12-06, by bulwahn
commenting out sledgehammer_mtd in Mutabelle
2010-12-06, by bulwahn
removing declaration in quickcheck to really enable exhaustive testing
2010-12-06, by bulwahn
adding timeout to try invocation in mutabelle
2010-12-06, by bulwahn
adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
2010-12-06, by bulwahn
replace `type_mapper` by the more adequate `type_lifting`
2010-12-06, by haftmann
moved bootstrap of type_lifting to Fun
2010-12-06, by haftmann
replace `type_mapper` by the more adequate `type_lifting`
2010-12-06, by haftmann
avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
2010-12-06, by wenzelm
IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
2010-12-05, by wenzelm
command 'notepad' replaces former 'example_proof';
2010-12-05, by wenzelm
prefer 'notepad' over 'example_proof';
2010-12-05, by wenzelm
merged
2010-12-05, by haftmann
more intimate definition of fold_list / fold_once in terms of fold
2010-12-04, by haftmann
canonical fold signature
2010-12-04, by haftmann
formal notepad without any result;
2010-12-04, by wenzelm
added Syntax.default_root;
2010-12-04, by wenzelm
eliminated obsolete Token.Malformed -- subsumed by Token.Error;
2010-12-04, by wenzelm
tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);
2010-12-04, by wenzelm
added Syntax.pretty_priority;
2010-12-04, by wenzelm
merged
2010-12-03, by haftmann
conventional point-free characterization of rsp_fold
2010-12-03, by haftmann
replaced memb by existing List.member
2010-12-03, by haftmann
explicit type constraint;
2010-12-03, by haftmann
tuned proposition
2010-12-03, by haftmann
lemma multiset_of_rev
2010-12-03, by haftmann
lemmas fold_remove1_split and fold_multiset_equiv
2010-12-03, by haftmann
minor tuning for release;
2010-12-03, by wenzelm
source files are always encoded as UTF-8;
2010-12-03, by wenzelm
eliminated fragile HTML.with_charset -- always use utf-8;
2010-12-03, by wenzelm
recoded latin1 as utf8;
2010-12-03, by wenzelm
removed old generated stuff;
2010-12-03, by wenzelm
comment;
2010-12-03, by wenzelm
update documentation
2010-12-03, by blanchet
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
2010-12-03, by blanchet
export more information about available SMT solvers
2010-12-03, by blanchet
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-03, by wenzelm
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
2010-12-02, by traytel
updated generated file;
2010-12-03, by wenzelm
removed confusing comments (cf. 500171e7aa59);
2010-12-03, by wenzelm
merged
2010-12-03, by wenzelm
removed outdated lint script
2010-12-03, by haftmann
merged
2010-12-03, by blanchet
compile
2010-12-03, by blanchet
run synchronous Auto Tools in parallel
2010-12-03, by blanchet
really fixed comment (cf. 7abeb749ae99)
2010-12-03, by krauss
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
2010-12-03, by huffman
eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
2010-12-03, by krauss
NEWS
2010-12-03, by bulwahn
only instantiate type variable if there exists some in quickcheck
2010-12-03, by bulwahn
fixing comment in library
2010-12-03, by bulwahn
adapting predicate_compile_quickcheck
2010-12-03, by bulwahn
adding a nice definition of Id_on for quickcheck and nitpick
2010-12-03, by bulwahn
adding code equation for finiteness of finite types
2010-12-03, by bulwahn
improving sledgehammer_tactic and adding relevance filtering to the tactic
2010-12-03, by bulwahn
adapting mutabelle
2010-12-03, by bulwahn
adapting SML_Quickcheck to recent changes
2010-12-03, by bulwahn
explaining quickcheck testers in the documentation
2010-12-03, by bulwahn
adapting quickcheck examples
2010-12-03, by bulwahn
improving presentation of quickcheck reports
2010-12-03, by bulwahn
declaring quickcheck testers as default after their setup
2010-12-03, by bulwahn
activating construction of exhaustive testing combinators
2010-12-03, by bulwahn
renamed generator into exhaustive
2010-12-03, by bulwahn
checking if parameter is name of a tester which allows e.g. quickcheck[random]
2010-12-03, by bulwahn
moving iteration of tests to the testers in quickcheck
2010-12-03, by bulwahn
removed dead test_term_small function in quickcheck
2010-12-03, by bulwahn
renamed parameter from generator to tester; quickcheck only applies one tester on invocation
2010-12-03, by bulwahn
adding configuration quickcheck_tester
2010-12-03, by bulwahn
adding smart quantifiers to exhaustive testing
2010-12-03, by bulwahn
adapting mutabelle
2010-12-03, by bulwahn
only handle TimeOut exception if used interactively
2010-12-03, by bulwahn
removed interrupt handling that violates Isabelle/ML exception model
2010-12-03, by bulwahn
corrected indentation
2010-12-03, by bulwahn
tuned
2010-12-03, by bulwahn
smallvalue_generator are defined quick via oracle or sound via function package
2010-12-03, by bulwahn
adding shorter output syntax for the finite types of quickcheck
2010-12-03, by bulwahn
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
2010-12-03, by bulwahn
changed order of lemmas to overwrite the general code equation with the nbe-specific one
2010-12-03, by bulwahn
adapt proofs to changed set_plus_image (cf. ee8d0548c148);
2010-12-03, by hoelzl
bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');
2010-12-03, by wenzelm
updated latex dependencies (cf. 7d88ebdce380);
2010-12-03, by wenzelm
tuned README;
2010-12-03, by wenzelm
isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;
2010-12-02, by wenzelm
proper theory name (cf. e84f82418e09);
2010-12-02, by wenzelm
merged;
2010-12-02, by wenzelm
merged
2010-12-02, by huffman
tuned cpodef code
2010-12-01, by huffman
reformulate lemma preorder.ex_ideal, and use it for typedefs
2010-12-01, by huffman
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
2010-12-02, by hoelzl
merged
2010-12-02, by haftmann
adapted expected value to more idiomatic numeral representation
2010-12-02, by haftmann
corrected representation for code_numeral numerals
2010-12-02, by haftmann
separate term_of function for integers -- more canonical representation of negative integers
2010-12-02, by haftmann
merged
2010-12-02, by hoelzl
Use coercions in Approximation (by Dmitriy Traytel).
2010-12-02, by hoelzl
more antiquotations;
2010-12-02, by wenzelm
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-12-02, by wenzelm
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-12-02, by wenzelm
merged
2010-12-02, by wenzelm
merged
2010-12-02, by hoelzl
generalized simple_functionD
2010-12-02, by hoelzl
Moved theorems to appropriate place.
2010-12-02, by hoelzl
Shorter definition for positive_integral.
2010-12-02, by hoelzl
Move SUP_commute, SUP_less_iff to HOL image;
2010-12-02, by hoelzl
Generalized simple_functionD and less_SUP_iff.
2010-12-01, by hoelzl
Tuned setup for borel_measurable with min, max and psuminf.
2010-12-01, by hoelzl
Replace algebra_eqI by algebra.equality;
2010-12-01, by hoelzl
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
2010-12-02, by blanchet
merged
2010-12-02, by wenzelm
coercions
2010-12-02, by nipkow
merged
2010-12-01, by nipkow
moved activation of coercion inference into RealDef and declared function real a coercion.
2010-12-01, by nipkow
Corrected IsaMakefile
2010-12-01, by hoelzl
merged
2010-12-01, by hoelzl
Updated NEWS
2010-12-01, by hoelzl
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
2010-12-01, by hoelzl
Support product spaces on sigma finite measures.
2010-12-01, by hoelzl
merged
2010-12-01, by haftmann
use type constructor as name for variable
2010-12-01, by haftmann
optional explicit prefix for type mapper theorems
2010-12-01, by haftmann
file for package tool type_mapper carries the same name as its Isar command
2010-12-01, by haftmann
merged
2010-12-01, by huffman
domain package generates non-authentic syntax rules for parsing only
2010-12-01, by huffman
builtin time bounds (again);
2010-12-02, by wenzelm
tuned;
2010-12-02, by wenzelm
more abstract handling of Time properties;
2010-12-01, by wenzelm
store tooltip-dismiss-delay as Double(seconds);
2010-12-01, by wenzelm
more abstract/uniform handling of time, preferring seconds as Double;
2010-12-01, by wenzelm
merged
2010-12-01, by wenzelm
NEWS
2010-12-01, by haftmann
just one HOLogic.mk_comp;
2010-12-01, by wenzelm
more direct use of binder_types/body_type;
2010-12-01, by wenzelm
tuned;
2010-12-01, by wenzelm
simplified HOL.eq simproc matching;
2010-12-01, by wenzelm
tuned;
2010-12-01, by wenzelm
just one Term.dest_funT;
2010-12-01, by wenzelm
activate subtyping/coercions in theory Complex_Main;
2010-12-01, by wenzelm
simplified equality on pairs of types;
2010-12-01, by wenzelm
more precise dependencies;
2010-12-01, by wenzelm
two-staged architecture for subtyping;
2010-11-29, by traytel
merged
2010-11-30, by huffman
change cpodef-generated cont_Rep rules to cont2cont format
2010-11-30, by huffman
internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules
2010-11-30, by huffman
remove gratuitous semicolons from ML code
2010-11-30, by huffman
add continuity lemma for List.map
2010-11-30, by huffman
simplify predomain instances
2010-11-30, by huffman
merged
2010-11-30, by boehmes
split up Z3 models into constraints on free variables and constant definitions;
2010-11-30, by boehmes
code preprocessor setup for numerals on word type;
2010-11-30, by haftmann
merged
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy
2010-11-30, by haftmann
adapted fragile proof
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
2010-11-30, by haftmann
adaptions to changes in Equiv_Relation.thy
2010-11-30, by haftmann
merged
2010-11-30, by haftmann
more systematic and compact proofs on type relation operators using natural deduction rules
2010-11-30, by haftmann
adapted proofs to slightly changed definitions of congruent(2)
2010-11-30, by haftmann
reorienting iff in Quotient_rel prevents simplifier looping;
2010-11-29, by haftmann
replaced slightly odd locale congruent2 by plain definition
2010-11-29, by haftmann
replaced slightly odd locale congruent by plain definition
2010-11-29, by haftmann
equivI has replaced equiv.intro
2010-11-29, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-29, by haftmann
moved generic definitions about relations from Quotient.thy to Predicate;
2010-11-29, by haftmann
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
2010-11-29, by haftmann
simplify proof of LIMSEQ_unique
2010-11-30, by huffman
use new 'file' antiquotation for reference to Dedekind_Real.thy
2010-11-30, by huffman
merged
2010-11-30, by huffman
instance list :: (discrete_cpo) discrete_cpo;
2010-11-29, by huffman
merged
2010-11-30, by boehmes
also support higher-order rules for Z3 proof reconstruction
2010-11-29, by boehmes
merged
2010-11-29, by wenzelm
less ghc-specific pragma
2010-11-29, by haftmann
tuned
2010-11-29, by haftmann
updated generated files;
2010-11-29, by wenzelm
added document antiquotation @{file};
2010-11-29, by wenzelm
Parse.liberal_name for document antiquotations and attributes;
2010-11-28, by wenzelm
ML results: enter before printing (cf. Poly/ML SVN 1218);
2010-11-28, by wenzelm
merged
2010-11-28, by wenzelm
merged
2010-11-28, by huffman
merged
2010-11-28, by huffman
change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec
2010-11-28, by huffman
add lemma cont2cont_if_bottom
2010-11-27, by huffman
added Parse.literal_fact with proper inner_syntax markup (source position);
2010-11-28, by wenzelm
tuned signature;
2010-11-28, by wenzelm
less frequent sidekick parsing, which is relatively slow;
2010-11-28, by wenzelm
basic setup for bundled Java runtime;
2010-11-28, by wenzelm
updated reference platforms;
2010-11-28, by wenzelm
merged
2010-11-28, by wenzelm
merged
2010-11-28, by nipkow
gave more standard finite set rules simp and intro attribute
2010-11-28, by nipkow
more permissive Isabelle_System.mkdir;
2010-11-28, by wenzelm
added 'syntax_declaration' command;
2010-11-28, by wenzelm
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
2010-11-28, by wenzelm
superficial tuning;
2010-11-28, by wenzelm
updated versions;
2010-11-28, by wenzelm
recovered Isabelle2009-2 NEWS -- published part is read-only;
2010-11-28, by wenzelm
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
avoid catch-all exception handling;
2010-11-02, by wenzelm
eliminated fragile catch-all pattern, based on educated guess about the intended exception;
2010-11-02, by wenzelm
Attribute map_function -> coercion_map;
2010-11-02, by traytel
syntax category "real" subsumes plain "int";
2010-10-31, by wenzelm
merged
2010-10-31, by nipkow
Plus -> Sum_Type.Plus
2010-10-29, by nipkow
Minor reformat.
2010-10-31, by ballarin
support for real valued preferences;
2010-10-30, by wenzelm
support for real valued configuration options;
2010-10-30, by wenzelm
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
2010-10-30, by wenzelm
merged
2010-10-29, by wenzelm
added rule let_mono
2010-10-29, by krauss
CONTRIBUTORS;
2010-10-29, by wenzelm
more sharing of operations, without aliases;
2010-10-29, by wenzelm
simplified data lookup;
2010-10-29, by wenzelm
export declarations by default, to allow other ML packages by-pass concrete syntax;
2010-10-29, by wenzelm
proper signature constraint for ML structure;
2010-10-29, by wenzelm
proper header;
2010-10-29, by wenzelm
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
2010-10-29, by wenzelm
updated SMT certificates
2010-10-29, by boehmes
eta-expand built-in constants; also rewrite partially applied natural number terms
2010-10-29, by boehmes
optionally drop assumptions which cannot be preprocessed
2010-10-29, by boehmes
added crafted list of SMT built-in constants
2010-10-29, by boehmes
clarified error message
2010-10-29, by boehmes
tuned
2010-10-29, by boehmes
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
2010-10-29, by boehmes
merged
2010-10-29, by wenzelm
added listrel1
2010-10-29, by nipkow
hide Sum_Type.Plus
2010-10-29, by nipkow
merged
2010-10-29, by wenzelm
added user aliasses (still unclear how to specify names with whitespace contained)
2010-10-29, by haftmann
merged
2010-10-29, by haftmann
tuned structure of theory
2010-10-29, by haftmann
remove term_of equations for Heap type explicitly
2010-10-29, by haftmann
no need for setting up the kodkodi environment since Kodkodi 1.2.9
2010-10-29, by blanchet
fixed order of quantifier instantiation in new Skolemizer
2010-10-29, by blanchet
restructure Skolemization code slightly
2010-10-29, by blanchet
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
2010-10-29, by blanchet
more work on new Skolemizer without Hilbert_Choice
2010-10-29, by blanchet
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
2010-10-29, by blanchet
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
2010-10-29, by blanchet
make handling of parameters more robust, by querying the goal
2010-10-29, by blanchet
actually pass "verbose" argument
2010-10-29, by haftmann
eliminated obsolete \_ escape;
2010-10-29, by wenzelm
eliminated obsolete \_ escapes in rail environments;
2010-10-29, by wenzelm
proper markup of formal text;
2010-10-29, by wenzelm
merged
2010-10-29, by wenzelm
hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
2010-10-29, by krauss
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
2010-10-29, by blanchet
merged
2010-10-29, by Lars Noschinski
Remove unnecessary premise of mult1_union
2010-09-22, by Lars Noschinski
adapting HOL-Mutabelle to changes in quickcheck
2010-10-29, by bulwahn
NEWS
2010-10-29, by bulwahn
changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
2010-10-29, by bulwahn
updating documentation on quickcheck in the Isar reference
2010-10-29, by bulwahn
merged
2010-10-28, by bulwahn
adding a simple check to only run with a SWI-Prolog version known to work
2010-10-28, by bulwahn
tuned messages;
2010-10-28, by wenzelm
discontinued obsolete ML antiquotation @{theory_ref};
2010-10-28, by wenzelm
tuned;
2010-10-28, by wenzelm
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
2010-10-28, by wenzelm
type attribute is derived concept outside the kernel;
2010-10-28, by wenzelm
preserve original source position of exn;
2010-10-28, by wenzelm
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
2010-10-28, by wenzelm
use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
2010-10-28, by wenzelm
added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
2010-10-28, by wenzelm
eliminated dead code;
2010-10-28, by wenzelm
tuned white-space;
2010-10-28, by wenzelm
merged
2010-10-28, by nipkow
added lemmas about listrel(1)
2010-10-28, by nipkow
tuned;
2010-10-28, by wenzelm
merged
2010-10-28, by wenzelm
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
2010-10-28, by blanchet
merged
2010-10-28, by blanchet
clear identification
2010-10-28, by blanchet
clear identification;
2010-10-28, by blanchet
clear identification
2010-10-28, by blanchet
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
2010-10-27, by blanchet
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
2010-10-27, by blanchet
generalize to handle any prover (not just E)
2010-10-27, by blanchet
merged
2010-10-27, by huffman
make domain package work with non-cpo argument types
2010-10-27, by huffman
make op -->> infixr, to match op --->
2010-10-27, by huffman
use Named_Thms instead of Theory_Data for some domain package theorems
2010-10-26, by huffman
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
2010-10-26, by huffman
use Term.add_tfreesT
2010-10-26, by huffman
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
2010-10-24, by huffman
rename constant 'one_when' to 'one_case'
2010-10-24, by huffman
merged
2010-10-27, by haftmann
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
2010-10-27, by haftmann
regenerated keyword file
2010-10-27, by krauss
made SML/NJ happy
2010-10-27, by boehmes
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
2010-10-26, by blanchet
better list of irrelevant SMT constants
2010-10-26, by blanchet
if "debug" is on, print list of relevant facts (poweruser request);
2010-10-26, by blanchet
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26, by blanchet
"Nitpick" -> "Sledgehammer";
2010-10-26, by blanchet
merge
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
remove needless context argument;
2010-10-26, by blanchet
use proper context
2010-10-26, by boehmes
trace assumptions before giving them to the SMT solver
2010-10-26, by boehmes
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
2010-10-26, by boehmes
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
2010-10-26, by boehmes
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
2010-10-26, by haftmann
fixed typo
2010-10-26, by krauss
merged
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
2010-10-26, by blanchet
tuning
2010-10-26, by blanchet
merged
2010-10-26, by haftmann
consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts
2010-10-26, by haftmann
more general treatment of type argument in code certificates for operations on abstract types
2010-10-26, by haftmann
partial_function is a declaration command
2010-10-26, by haftmann
merged
2010-10-26, by blanchet
proper error handling for SMT solvers in Sledgehammer
2010-10-26, by blanchet
NEWS
2010-10-26, by krauss
merge
2010-10-26, by blanchet
integrated "smt" proof method with Sledgehammer
2010-10-26, by blanchet
fixed confusion introduced in 008dc2d2c395
2010-10-26, by krauss
merged
2010-10-26, by blanchet
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-26, by blanchet
merged
2010-10-26, by haftmann
tuned
2010-10-26, by haftmann
merged
2010-10-26, by krauss
use partial_function instead of MREC combinator; curried rev'
2010-10-26, by krauss
added Heap monad instance of partial_function package
2010-10-26, by krauss
added Spec_Rule declaration to partial_function
2010-10-26, by krauss
basic documentation for command partial_function
2010-10-26, by krauss
remove outdated "(otherwise)" syntax from manual
2010-10-26, by krauss
declare recursive equation as ".simps", in accordance with other packages
2010-10-26, by krauss
merged
2010-10-26, by haftmann
dropped accidental doubled computation
2010-10-26, by haftmann
optionally force the remote version of an SMT solver to be executed
2010-10-26, by boehmes
tuned
2010-10-26, by boehmes
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
2010-10-26, by boehmes
changed SMT configuration options; updated SMT certificates
2010-10-26, by boehmes
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
2010-10-26, by boehmes
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
2010-10-26, by boehmes
merged
2010-10-26, by blanchet
merge
2010-10-26, by blanchet
clearer error messages
2010-10-26, by blanchet
renaming
2010-10-26, by blanchet
back again to non-Apple font rendering (cf. 4977324373f2);
2010-10-28, by wenzelm
dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible;
2010-10-28, by wenzelm
disable broken popups for now;
2010-10-26, by wenzelm
tuned;
2010-10-26, by wenzelm
do not handle arbitrary exceptions;
2010-10-26, by wenzelm
merged
2010-10-26, by wenzelm
Code_Runtime.trace
2010-10-26, by haftmann
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
2010-10-26, by wenzelm
merged
2010-10-26, by wenzelm
improved English
2010-10-26, by blanchet
whitespace tuning
2010-10-26, by blanchet
no need to encode theorem number twice in skolem names
2010-10-26, by blanchet
tuning
2010-10-26, by blanchet
make SML/NJ happy
2010-10-26, by blanchet
relaxing the filtering condition for getting specifications from Spec_Rules
2010-10-25, by bulwahn
adding new predicate compiler files to the IsaMakefile
2010-10-25, by bulwahn
using mode_eq instead of op = for lookup in the predicate compiler
2010-10-25, by bulwahn
renaming split_modeT' to split_modeT
2010-10-25, by bulwahn
options as first argument to check functions
2010-10-25, by bulwahn
changing test parameters in examples to get to a result within the global timelimit
2010-10-25, by bulwahn
adding a global fixed timeout to quickcheck
2010-10-25, by bulwahn
adding a global time limit to the values command
2010-10-25, by bulwahn
explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
2010-10-25, by wenzelm
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25, by wenzelm
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-25, by wenzelm
explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-10-25, by wenzelm
export main ML entry by default;
2010-10-25, by wenzelm
observe Isabelle/ML coding standards;
2010-10-25, by wenzelm
merged
2010-10-25, by wenzelm
significantly improved Isabelle/Isar implementation manual;
2010-10-25, by wenzelm
misc tuning;
2010-10-25, by wenzelm
removed some remains of Output.debug (follow-up to fce2202892c4);
2010-10-25, by wenzelm
recovered some odd two-dimensional layout;
2010-10-25, by wenzelm
merged
2010-10-25, by haftmann
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
2010-10-25, by haftmann
moved sledgehammer to Plain; tuned dependencies
2010-10-25, by haftmann
CONTRIBUTORS
2010-10-25, by haftmann
merge
2010-10-25, by blanchet
merged
2010-10-25, by blanchet
updated keywords
2010-10-25, by blanchet
introduced manual version of "Auto Solve" as "solve_direct"
2010-10-25, by blanchet
make "sledgehammer_params" work on single-threaded platforms
2010-10-25, by blanchet
tuning
2010-10-22, by blanchet
handle timeouts (to prevent failure from other threads);
2010-10-22, by blanchet
update keywords
2010-10-25, by haftmann
some partial_function examples
2010-10-25, by krauss
added ML antiquotation @{assert};
2010-10-25, by wenzelm
updated keywords;
2010-10-25, by wenzelm
integrated partial_function into HOL-Plain
2010-10-23, by krauss
first version of partial_function package
2010-10-23, by krauss
Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem
2010-10-23, by krauss
merged
2010-10-25, by bulwahn
splitting Hotel Key card example into specification and the two tests for counter example generation
2010-10-22, by bulwahn
adding generator quickcheck
2010-10-22, by bulwahn
restructuring values command and adding generator compilation
2010-10-22, by bulwahn
moving general functions from core_data to predicate_compile_aux
2010-10-22, by bulwahn
updating to new notation in commented examples
2010-10-22, by bulwahn
merged
2010-10-24, by huffman
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
2010-10-24, by huffman
remove legacy comp_dbind option from domain package
2010-10-23, by huffman
change fixrec parser to not accept theorem names with (unchecked) option
2010-10-23, by huffman
tuned
2010-10-23, by huffman
rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd
2010-10-22, by huffman
add lemma strict3
2010-10-22, by huffman
do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas
2010-10-22, by huffman
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
2010-10-22, by huffman
direct instantiation unit :: discrete_cpo
2010-10-22, by huffman
remove finite_po class
2010-10-22, by huffman
simplify proofs about flift; remove unneeded lemmas
2010-10-22, by huffman
simplify proof
2010-10-22, by huffman
minimize imports
2010-10-21, by huffman
add type annotation to avoid warning
2010-10-21, by huffman
simplify some proofs, convert to Isar style
2010-10-21, by huffman
rename lemma spair_lemma to spair_Sprod
2010-10-21, by huffman
pcpodef (open) 'a lift
2010-10-21, by huffman
remove intro! attribute from {sinl,sinr}_defined
2010-10-21, by huffman
simplify proofs of ssumE, sprodE
2010-10-21, by huffman
merged
2010-10-24, by wenzelm
renamed nat_number
2010-10-24, by nipkow
nat_number -> eval_nat_numeral
2010-10-24, by nipkow
some cleanup in Function_Lib
2010-10-22, by krauss
merged
2010-10-22, by blanchet
compile
2010-10-22, by blanchet
added SMT solver to Sledgehammer docs
2010-10-22, by blanchet
more robust handling of "remote_" vs. non-"remote_" provers
2010-10-22, by blanchet
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
2010-10-22, by blanchet
replaced references with proper record that's threaded through
2010-10-22, by blanchet
fixed signature of "is_smt_solver_installed";
2010-10-22, by blanchet
renamed modules
2010-10-22, by blanchet
renamed files
2010-10-22, by blanchet
took out "smt"/"remote_smt" from default ATPs until they are properly implemented
2010-10-22, by blanchet
remove more needless code ("run_smt_solvers");
2010-10-22, by blanchet
got rid of duplicate functionality ("run_smt_solver_somehow");
2010-10-22, by blanchet
bring ATPs and SMT solvers more in line with each other
2010-10-22, by blanchet
make Sledgehammer minimizer fully work with SMT
2010-10-22, by blanchet
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
2010-10-22, by blanchet
first step in adding support for an SMT backend to Sledgehammer
2010-10-21, by blanchet
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-10-21, by blanchet
cosmetics
2010-10-21, by blanchet
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
2010-10-22, by krauss
Changed section title to please LaTeX.
2010-10-22, by hoelzl
temporary removed Predicate_Compile_Quickcheck_Examples from tests
2010-10-21, by bulwahn
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-10-21, by bulwahn
using a signature in core_data and moving some more functions to core_data
2010-10-21, by bulwahn
splitting large core file into core_data, mode_inference and predicate_compile_proof
2010-10-21, by bulwahn
added generator_dseq compilation for a sound depth-limited compilation with small value generators
2010-10-21, by bulwahn
for now safely but unpractically assume no predicate is terminating
2010-10-21, by bulwahn
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
2010-10-21, by bulwahn
adding option smart_depth_limiting to predicate compiler
2010-10-21, by bulwahn
merged
2010-10-20, by huffman
introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
2010-10-20, by huffman
add lemma lub_eq_bottom_iff
2010-10-20, by huffman
combine check_and_sort_domain with main function; rewrite much of the error-checking code
2010-10-20, by huffman
constructor arguments with selectors must have pointed types
2010-10-20, by huffman
simplify check_and_sort_domain; more meaningful variable names
2010-10-20, by huffman
replace fixrec 'permissive' mode with per-equation 'unchecked' option
2010-10-19, by huffman
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
2010-10-19, by huffman
simplify some proofs; remove some unused lists of lemmas
2010-10-19, by huffman
replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
2010-10-19, by huffman
eliminate constant 'coerce'; use 'prj oo emb' instead
2010-10-19, by huffman
simplify fixrec pattern match function
2010-10-19, by huffman
simplify some proofs
2010-10-17, by huffman
tuned
2010-10-19, by Christian Urban
added some facts about factorial and dvd, div and mod
2010-10-19, by bulwahn
removing something that probably slipped into the Quotient_List theory
2010-10-19, by bulwahn
Quotient package: partial equivalence introduction
2010-10-19, by Cezary Kaliszyk
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
2010-10-18, by Christian Urban
remove dead code
2010-10-16, by huffman
remove old uses of 'simp_tac HOLCF_ss'
2010-10-16, by huffman
merged
2010-10-16, by huffman
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
2010-10-16, by huffman
reimplement proof automation for coinduct rules
2010-10-16, by huffman
add functions mk_imp, mk_all
2010-10-16, by huffman
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
2010-10-15, by huffman
simplify automation of induct proof
2010-10-15, by huffman
add function mk_adm
2010-10-15, by huffman
rewrite proof automation for finite_ind; get rid of case_UU_tac
2010-10-15, by huffman
put constructor argument specs in constr_info type
2010-10-14, by huffman
avoid using Global_Theory.get_thm
2010-10-14, by huffman
include iso_info as part of constr_info type
2010-10-14, by huffman
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
2010-10-14, by huffman
add take_strict_thms field to take_info type
2010-10-14, by huffman
add record type synonym 'constr_info'
2010-10-14, by huffman
add function take_theorems
2010-10-14, by huffman
add type annotation to avoid warning
2010-10-14, by huffman
cleaned up Fun_Cpo.thy; deprecated a few theorem names
2010-10-13, by huffman
edit comments
2010-10-13, by huffman
remove unneeded lemmas Lift_exhaust, Lift_cases
2010-10-12, by huffman
move lemmas from Lift.thy to Cfun.thy
2010-10-12, by huffman
cleaned up Adm.thy
2010-10-12, by huffman
remove unneeded lemmas from Fun_Cpo.thy
2010-10-12, by huffman
remove unused lemmas
2010-10-12, by huffman
reformulate lemma cont2cont_lub and move to Cont.thy
2010-10-12, by huffman
remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
2010-10-12, by huffman
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
2010-10-11, by huffman
rename Ffun.thy to Fun_Cpo.thy
2010-10-11, by huffman
remove unused constant 'directed'
2010-10-11, by huffman
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
2010-10-11, by huffman
merged
2010-10-15, by paulson
prevention of self-referential type environments
2010-10-15, by paulson
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
2010-10-15, by Cezary Kaliszyk