Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+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.
killed legacy "neg_clausify" and "clausify"
2010-06-23, by blanchet
merged
2010-06-22, by blanchet
factor out TPTP format output into file of its own, to facilitate further changes
2010-06-22, by blanchet
merged
2010-06-22, by blanchet
turn on "natural form" filtering in the Mirabelle tests, to see how it performs
2010-06-22, by blanchet
missing "Unsynchronized" + make exception take a unit
2010-06-22, by blanchet
added code to optionally perform fact filtering on the original (non-CNF) formulas
2010-06-22, by blanchet
more cosmetics
2010-06-22, by blanchet
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
2010-06-22, by blanchet
canonical argument order
2010-06-22, by blanchet
leverage new data structure for handling "add:" and "del:"
2010-06-22, by blanchet
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
2010-06-22, by blanchet
merge "generic_prover" and "generic_tptp_prover"
2010-06-22, by blanchet
removed Sledgehammer's support for the DFG syntax;
2010-06-22, by blanchet
distinguish between "unknown" and "no Kodkodi installed" errors
2010-06-22, by blanchet
reintroduce new Sledgehammer polymorphic handling code;
2010-06-22, by blanchet
make the Nitpick_Example theory processable even when Kodkodi is not installed;
2010-06-22, by blanchet
Make latex happy
2010-06-23, by hoelzl
Quotient package now uses Partial Equivalence instead place of equivalence
2010-06-23, by Cezary Kaliszyk
Replace 'list_rel' by 'list_all2'; they are equivalent.
2010-06-23, by Cezary Kaliszyk
Proper treatment of non-inherited mixins.
2010-06-22, by ballarin
merged
2010-06-22, by hoelzl
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-06-21, by hoelzl
reredisable new polymorphic code
2010-06-22, by blanchet
merged
2010-06-21, by blanchet
beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later;
2010-06-21, by blanchet
back to post-release mode;
2010-06-21, by wenzelm
merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;
2010-06-21, by wenzelm
make Nitpick's unsound mode a bit more unsound
2010-06-21, by blanchet
sort cases on the proper key
2010-06-21, by blanchet
compile
2010-06-21, by blanchet
thread "full_types"
2010-06-21, by blanchet
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-21, by blanchet
clean up after fcc768dc9dd0
2010-06-21, by blanchet
adjusted Nitpick examples to latest changes + make them slightly faster
2010-06-21, by blanchet
optimized code generated for datatype cases + more;
2010-06-21, by blanchet
activated Scala code generator test
2010-06-21, by haftmann
added bot instances; tuned
2010-06-21, by haftmann
extensionality rule fset_eqI
2010-06-21, by haftmann
merged
2010-06-20, by haftmann
separate section for diagnostic commands
2010-06-20, by haftmann
more binding; avoid arcane Rep and Abs prefixes
2010-06-19, by haftmann
cleanup of typecopy package
2010-06-19, by haftmann
quickcheck for fsets
2010-06-19, by haftmann
merged
2010-06-18, by nipkow
added pigeonhole lemmas
2010-06-18, by nipkow
merged
2010-06-18, by haftmann
tuned whitespace; dropped dead code
2010-06-18, by haftmann
code_simp: only succeed on real progress
2010-06-18, by haftmann
prefer fold over foldl
2010-06-18, by haftmann
conclude simplification with default simpset
2010-06-18, by haftmann
drop subsumed default equations (requires a little bit unfortunate laziness)
2010-06-18, by haftmann
avoid Scala legacy operations
2010-06-18, by haftmann
prefer fold over foldl
2010-06-18, by haftmann
made List.thy a join point in the theory graph
2010-06-18, by haftmann
tuned set_replicate lemmas
2010-06-18, by nipkow
merged
2010-06-18, by nipkow
added lemmas
2010-06-18, by nipkow
dropped dead code
2010-06-18, by haftmann
replaced unreliable metis proof
2010-06-17, by haftmann
rev is reverse in Haskell
2010-06-17, by haftmann
first serious draft of a scala code generator
2010-06-17, by haftmann
more precise code
2010-06-17, by haftmann
explicit type variable arguments for constructors
2010-06-17, by haftmann
transitive superclasses were also only a misunderstanding
2010-06-17, by haftmann
formal introduction of transitive superclasses
2010-06-17, by haftmann
dropped obscure type argument weakening mapping -- was only a misunderstanding
2010-06-17, by haftmann
added simp evaluator
2010-06-17, by haftmann
merged
2010-06-17, by haftmann
added code_simp infrastructure
2010-06-15, by haftmann
tuned whitespace
2010-06-15, by haftmann
maintain cong rules for case combinators; more precise permissiveness
2010-06-15, by haftmann
drop function definitions of combinators
2010-06-15, by haftmann
maintain cong rules for case combinators
2010-06-15, by haftmann
formal introduction of case cong
2010-06-15, by haftmann
found missing beta-eta-contraction
2010-06-15, by blanchet
added missing Umlaut
2010-06-15, by blanchet
make example run a bit faster (might help atbroy102)
2010-06-15, by blanchet
merged
2010-06-15, by haftmann
tuned documents
2010-06-15, by haftmann
teaked naming of superclass projections
2010-06-14, by haftmann
added lemma funpow_mult
2010-06-14, by haftmann
extended bib
2010-06-14, by haftmann
updated generated code
2010-06-14, by haftmann
added reference
2010-06-14, by haftmann
subsection on locale interpretation
2010-06-14, by haftmann
explicitly name and note equations for class eq
2010-06-14, by haftmann
use various predefined Haskell operations when generating code
2010-06-14, by haftmann
NEWS
2010-06-14, by haftmann
tuned internal order
2010-06-14, by haftmann
dropped unused bindings
2010-06-14, by haftmann
corrected syntax diagram
2010-06-14, by haftmann
turn off new polymorphism code again -- a new issue popped up
2010-06-14, by blanchet
missing case
2010-06-14, by blanchet
A function called "untyped_aconv" shouldn't look at the bound names!
2010-06-14, by blanchet
no point in introducing combinators for inlined Skolem functions
2010-06-14, by blanchet
better error reporting for Vampire
2010-06-14, by blanchet
expect SPASS 3.7, and give a friendly warning if an older version is used
2010-06-14, by blanchet
improve ATP-specific error messages
2010-06-14, by blanchet
merged
2010-06-14, by haftmann
removed simplifier congruence rule of "prod_case"
2010-06-14, by haftmann
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-14, by blanchet
merged
2010-06-12, by haftmann
declare lexn.simps [code del]
2010-06-12, by haftmann
declare lex_prod_def [code del]
2010-06-11, by haftmann
modernized specifications
2010-06-11, by haftmann
avoid references to old constdefs
2010-06-11, by haftmann
merged
2010-06-12, by blanchet
disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved
2010-06-12, by blanchet
"raise Fail" for internal errors + one new internal error (instead of "Match")
2010-06-12, by blanchet
make test work again (broken since 09467cdfa198?)
2010-06-11, by blanchet
adjust Nitpick example to follow latest wave of renamings
2010-06-11, by blanchet
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-11, by blanchet
beta-eta-contract, to respect "first_order_match"'s specification;
2010-06-11, by blanchet
adjust Nitpick's handling of "<" on "rat"s and "reals"
2010-06-11, by blanchet
remove needless variables
2010-06-11, by blanchet
hide sum explicitly
2010-06-11, by haftmann
merged
2010-06-10, by haftmann
adjust popular symbolic type constructors
2010-06-10, by haftmann
tailored set of code equations manually
2010-06-10, by haftmann
tuned quotes, antiquotations and whitespace
2010-06-10, by haftmann
moved inductive_codegen to place where product type is available; tuned structure name
2010-06-10, by haftmann
qualified type "*"; qualified constants Pair, fst, snd, split
2010-06-10, by haftmann
tuned quotes, antiquotations and whitespace
2010-06-08, by haftmann
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-06-08, by haftmann
Adapted Mirabelle script (cf. f60e4dd6d76f)
2010-06-10, by krauss
merged
2010-06-08, by haftmann
more consistent naming aroud type classes and instances
2010-06-07, by haftmann
back to non-release mode;
2010-06-07, by wenzelm
removed obsolete test tags;
2010-06-21, by wenzelm
Added tag Isabelle2009-2 for changeset 35815ce9218a
2010-06-21, by wenzelm
final tuning;
Isabelle2009-2
2010-06-21, by wenzelm
corrected syntax diagram
2010-06-14, by haftmann
Adapted Mirabelle script (cf. f60e4dd6d76f)
2010-06-10, by krauss
Added tag isa2009-2-test3 for changeset 0eacedd5f780
2010-06-14, by wenzelm
merged
2010-06-14, by wenzelm
NEWS: IsabelleText font;
2010-06-11, by wenzelm
Pretty.string_of (in Scala): actually observe margin/metric;
2010-06-13, by wenzelm
tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
2010-06-13, by wenzelm
tuned tooltips;
2010-06-11, by wenzelm
obsolete;
2010-06-09, by wenzelm
explicit treatment of empty exception block, which could lead to confusing output (e.g. in the theory loader), or even prevent error output altogether;
2010-06-09, by wenzelm
contrib/README;
2010-06-09, by wenzelm
removed outdated/confusing INSTALL file;
2010-06-09, by wenzelm
clarified font_family vs. font_family_default;
2010-06-08, by wenzelm
disable set_styles for now -- there are still some race conditions of PropertiesChanged vs. TextArea painting (NB: without it Isabelle_Token_Marker will crash if sub/superscript is actually used);
2010-06-08, by wenzelm
Added tag isa2009-2-test2 for changeset dfca6c4cd1e8
2010-06-07, by wenzelm
more uniform treatment of options and attributes, preferring formal markup over old-style LaTeX macros;
2010-06-07, by wenzelm
merged;
2010-06-07, by wenzelm
Tuned.
2010-06-07, by berghofe
Documented changes in induct, cases, and nominal_induct method.
2010-06-07, by berghofe
merged
2010-06-07, by wenzelm
made SML/NJ happy again;
2010-06-07, by wenzelm
recovered some untested theories;
2010-06-07, by wenzelm
proper target directory;
2010-06-07, by wenzelm
refer to isabelle-release branch;
2010-06-07, by wenzelm
no symlinks;
2010-06-07, by wenzelm
merged
2010-06-07, by wenzelm
tuned ANNOUNCEMENT;
2010-06-07, by wenzelm
more NEWS;
2010-06-07, by wenzelm
more NEWS;
2010-06-07, by wenzelm
merged
2010-06-07, by blanchet
cosmetics
2010-06-07, by blanchet
renaming
2010-06-05, by blanchet
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
2010-06-05, by blanchet
fix remote Vampire diagnosis
2010-06-05, by blanchet
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
2010-06-05, by blanchet
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
2010-06-05, by blanchet
single heaps archive;
2010-06-06, by wenzelm
merged
2010-06-06, by wenzelm
tuned;
2010-06-06, by wenzelm
removed obsolete dry-run option;
2010-06-06, by wenzelm
Added tag isa2009-2-test1 for changeset d1cdbc7524b6
2010-06-06, by wenzelm
merged
2010-06-05, by haftmann
avoid "$"
2010-06-04, by haftmann
tuned whitespace
2010-06-04, by haftmann
avoid flowerish abbreviation
2010-06-04, by haftmann
merged
2010-06-04, by wenzelm
merge
2010-06-04, by blanchet
don't raise Option.Option if assumptions contain schematic variables
2010-06-04, by blanchet
recongize one more outcome string for "remote_vampire"
2010-06-04, by blanchet
"print_vars_terms" wasn't doing its job properly;
2010-06-04, by blanchet
merged
2010-06-04, by blanchet
made "clausify" attribute a legacy feature;
2010-06-04, by blanchet
made "neg_clausify" a legacy feature
2010-06-04, by blanchet
kill active Sledgehammer threads when running minimize, to avoid confusing the user with too much output
2010-06-04, by blanchet
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
2010-06-04, by blanchet
fix bugs in Sledgehammer's Isar proof "redirection" code
2010-06-04, by blanchet
handle Vampire's definitions smoothly
2010-06-02, by blanchet
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
2010-06-02, by blanchet
honor "xsymbols"
2010-06-02, by blanchet
kill another neg_clausify proof
2010-06-02, by blanchet
show types in Isar proofs, but not for free variables;
2010-06-02, by blanchet
give more helpful error message
2010-06-02, by blanchet
first proposal for a announcement
2010-06-04, by haftmann
NEWS (more strict internal axioms/defs format)
2010-06-04, by krauss
one all-inclusive bundle for each platform;
2010-06-04, by wenzelm
more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);
2010-06-04, by wenzelm
tuned warning;
2010-06-04, by wenzelm
less ambitious settings;
2010-06-04, by wenzelm
spelling;
2010-06-04, by wenzelm
do not open Proofterm, which is very ould style;
2010-06-03, by wenzelm
eliminated ML structure alias;
2010-06-03, by wenzelm
tuned default perspective;
2010-06-03, by wenzelm
tracing in aliceblue;
2010-06-03, by wenzelm
discontinued obsolete Isar.context() -- long superseded by @{context};
2010-06-03, by wenzelm
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
2010-06-03, by wenzelm
allow qualified names;
2010-06-03, by wenzelm
CONTRIBUTORS
2010-06-03, by krauss
clarified
2010-06-03, by krauss
mention unconstrain in NEWS
2010-06-03, by krauss
merged
2010-06-02, by haftmann
hide default, map_entry, map_default
2010-06-02, by haftmann
improved parallelism of proof term normalization;
2010-06-02, by wenzelm
always unconstrain thm proofs;
2010-06-02, by wenzelm
replaced ML pokes by explicit usedir -p;
2010-06-02, by wenzelm
merged
2010-06-02, by haftmann
absolute import -- must work with Main.thy / HOL-Proofs
2010-06-02, by haftmann
avoid duplicate import
2010-06-02, by haftmann
HOL-Proofs is based in Main.thy
2010-06-02, by haftmann
dropped lemma duplicate
2010-06-02, by haftmann
msetprod_empty, msetprod_singleton
2010-06-02, by haftmann
induction over non-empty lists
2010-06-02, by haftmann
removed dependency of Euclid on Old_Number_Theory
2010-06-02, by haftmann
modernized
2010-06-02, by haftmann
removed obsolete usedir -p 1 option;
2010-06-02, by wenzelm
actually test smlnj;
2010-06-02, by wenzelm
updated keywords;
2010-06-02, by wenzelm
Added tag isa2009-2-test0 for changeset 935c75359742
2010-06-02, by wenzelm
more CONTRIBUTORS;
2010-06-02, by wenzelm
merged
2010-06-02, by wenzelm
Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
2010-06-02, by wenzelm
merged
2010-06-02, by nipkow
added lemmas
2010-06-02, by nipkow
merged
2010-06-02, by blanchet
merge
2010-06-02, by blanchet
fix parameter settings
2010-06-02, by blanchet
merged
2010-06-01, by blanchet
merged
2010-06-01, by blanchet
update NEWS
2010-06-01, by blanchet
fix Nitpick soundness bug regarding The and Eps
2010-06-01, by blanchet
added examples/tests for THE and SOME
2010-06-01, by blanchet
cosmetics
2010-06-01, by blanchet
adapt example
2010-06-01, by blanchet
fix code that used to raise an exception if bound variables were given a finite function type, because the old vs. new bound variable types were confused
2010-06-01, by blanchet
improved precision of "set" based on an example from Lukas
2010-06-01, by blanchet
remove debug output
2010-06-01, by blanchet
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-06-01, by blanchet
subsumed by NEWS -- for older history, see previous versions of Nitpick
2010-06-01, by blanchet
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
2010-06-01, by blanchet
honor xsymbols in Nitpick
2010-06-01, by blanchet
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-06-01, by blanchet
document new option
2010-06-01, by blanchet
make Nitpick handle multiple typedef entries for same typedef
2010-06-01, by blanchet
remove comment
2010-06-01, by blanchet
thread along context instead of theory for typedef lookup
2010-06-01, by blanchet
obsolete FIXME
2010-05-31, by blanchet
move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it;
2010-05-31, by blanchet
don't include any axioms for "TYPE" in Nitpick
2010-05-31, by blanchet
dropped obsolete script
2010-06-02, by haftmann
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
2010-06-02, by wenzelm
merged
2010-06-02, by haftmann
avoid store flag in add_* operations
2010-06-01, by haftmann
arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
2010-06-01, by wenzelm
merged
2010-06-01, by wenzelm
do not expose store flag of AxClass.add_*
2010-06-01, by haftmann
merged
2010-06-01, by haftmann
adapted to changes
2010-06-01, by haftmann
capitalized type variables; added yield as keyword
2010-06-01, by haftmann
brackify_infix etc.: no break before infix operator -- eases survival in Scala
2010-06-01, by haftmann
basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;
2010-06-01, by wenzelm
use local /home/isatest/polyml-5.3.0 on atbroy102 to avoid problems with the SMB filesystem via homebroy;
2010-06-01, by wenzelm
uniform ML environment setup for Isar and PG;
2010-06-01, by wenzelm
merged
2010-06-01, by berghofe
Renamed TypeInfer to Type_Infer.
2010-06-01, by berghofe
merged
2010-06-01, by berghofe
assign now applies meet before update_new to avoid misleading error message.
2010-06-01, by berghofe
Tuned.
2010-06-01, by berghofe
Adapted to new format of proof terms containing explicit proofs of class membership.
2010-06-01, by berghofe
classrel and arity theorems are now stored under proper name in theory. add_arity and
2010-06-01, by berghofe
- outer_constraints with original variable names, to ensure that argsP is consistent with args
2010-06-01, by berghofe
outer_constraints with original variable names, to ensure that argsP is consistent with args
2010-06-01, by berghofe
- Equality check on propositions after lookup of theorem now takes type variable
2010-06-01, by berghofe
Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.
2010-06-01, by berghofe
- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which
2010-06-01, by berghofe
merged
2010-06-01, by wenzelm
merged
2010-06-01, by haftmann
corrected printing of characters
2010-06-01, by haftmann
corrected implementation
2010-06-01, by haftmann
added Scala code setup
2010-06-01, by haftmann
tuned code setup
2010-06-01, by haftmann
keep structure ThyLoad for the sake of Proof General;
2010-06-01, by wenzelm
added random instance for word
2010-06-01, by haftmann
notes on Isabelle/jEdit;
2010-05-31, by wenzelm
remove presently unused Isabelle application;
2010-05-31, by wenzelm
modernized some structure names, keeping a few legacy aliases;
2010-05-31, by wenzelm
merged
2010-05-31, by wenzelm
merge
2010-05-31, by blanchet
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
2010-05-31, by blanchet
updated generated files
2010-05-31, by haftmann
clarified
2010-05-31, by haftmann
adjusted
2010-05-31, by haftmann
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
2010-05-31, by wenzelm
Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;
2010-05-31, by wenzelm
merged
2010-05-31, by wenzelm
Typo in locales tutorial.
2010-05-30, by ballarin
Theory_Target.pretty: more markup;
2010-05-31, by wenzelm
tuned abbrevs for long arrows, according to usual ASCII syntax;
2010-05-31, by wenzelm
more flexibile font size via CSS <style> instead of old <font> element;
2010-05-31, by wenzelm
tuned;
2010-05-31, by wenzelm
control tooltip font via Swing HTML, with tooltip-font-size property;
2010-05-30, by wenzelm
added HTML.encode (in Scala), similar to HTML.output in ML;
2010-05-30, by wenzelm
one extra space to accomodate symbolic indentifiers etc.;
2010-05-30, by wenzelm
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
2010-05-30, by wenzelm
more detailed token markup, including command kind as sub_kind;
2010-05-30, by wenzelm
tuned;
2010-05-30, by wenzelm
separate markup for ML delimiters;
2010-05-30, by wenzelm
less pschedelic token markup;
2010-05-30, by wenzelm
simplified command/keyword markup;
2010-05-30, by wenzelm
markup non-identifier keyword as operator;
2010-05-30, by wenzelm
Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;
2010-05-30, by wenzelm
more basic default behaviour of ENTER, HOME, END;
2010-05-30, by wenzelm
tuned messages;
2010-05-29, by wenzelm
do not highlight ignored command spans;
2010-05-29, by wenzelm
more explicit handling of document;
2010-05-29, by wenzelm
explicit markup for forked goals, as indicated by Goal.fork;
2010-05-29, by wenzelm
avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;
2010-05-29, by wenzelm
define_state/new_state: provide state immediately, which is now lazy;
2010-05-29, by wenzelm
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
2010-05-29, by wenzelm
future result: retain plain Interrupt for vacuous group exceptions;
2010-05-29, by wenzelm
remove two examples, now that the definition of "fst" and "snd" has changed
2010-05-28, by blanchet
merged
2010-05-28, by wenzelm
Got rid of a warning about duplicate rewrite rules.
2010-05-28, by webertj
accumulate only local results -- no proper history support yet;
2010-05-28, by wenzelm
avoid deprecated Iterator.fromArray;
2010-05-28, by wenzelm
more compiler warnings;
2010-05-28, by wenzelm
eliminated hard tabs;
2010-05-28, by wenzelm
assume given SCALA_HOME, e.g. from component settings or external setup;
2010-05-28, by wenzelm
merged
2010-05-28, by wenzelm
merged
2010-05-28, by blanchet
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-28, by blanchet
Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
2010-05-27, by blanchet
make Nitpick "show_all" option behave less surprisingly
2010-05-27, by blanchet
merged
2010-05-28, by haftmann
avoid reference to thm PairE
2010-05-28, by haftmann
more coherent theory structure; tuned headings
2010-05-28, by haftmann
made SML/NJ quite happy;
2010-05-28, by wenzelm
reuse main view.font from jEdit;
2010-05-28, by wenzelm
deleted some old fonts;
2010-05-28, by wenzelm
also set font for printing, which actually works out of the box;
2010-05-28, by wenzelm
lib/Tools/makeall does not hardiwre logics;
2010-05-28, by wenzelm
discontinued Sun/Solaris tests;
2010-05-28, by wenzelm
some updates for release;
2010-05-28, by wenzelm
merged
2010-05-27, by wenzelm
added function update examples and set examples
2010-05-27, by boehmes
updated SMT certificates
2010-05-27, by boehmes
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
2010-05-27, by boehmes
merged
2010-05-27, by boehmes
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-27, by boehmes
made script executable
2010-05-27, by boehmes
use Z3's builtin support for div and mod
2010-05-27, by boehmes
moved SMT into the HOL image
2010-05-27, by boehmes
slightly odd workaround to ignore markup that is typically displaced;
2010-05-27, by wenzelm
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
2010-05-27, by wenzelm
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
2010-05-27, by wenzelm
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27, by wenzelm
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27, by wenzelm
misc updates for release;
2010-05-27, by wenzelm
constant Rat.normalize needs to be qualified;
2010-05-27, by wenzelm
merged
2010-05-27, by wenzelm
merged
2010-05-27, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
normalized references to constant "split"
2010-05-26, by haftmann
Revise locale test theory layout.
2010-05-26, by ballarin
Merge mixins of distinct interpretations with same base.
2010-05-26, by ballarin
indicate prospective properties;
2010-05-27, by wenzelm
clarified auto_update vs. update;
2010-05-27, by wenzelm
more reactive message handling, notably for follow_caret mode;
2010-05-27, by wenzelm
Command.toString: include id for debugging;
2010-05-27, by wenzelm
merged
2010-05-26, by wenzelm
refer to polyml-5.3.0-old for ppc-darwin;
2010-05-26, by wenzelm
try logical and theory abstraction before full abstraction (avoids warnings of linarith)
2010-05-26, by boehmes
updated SMT certificates
2010-05-26, by boehmes
hide constants and types introduced by SMT,
2010-05-26, by boehmes
more convenient order of code equations
2010-05-26, by haftmann
misc updates for release;
2010-05-26, by wenzelm
eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-25, by wenzelm
moved ML files where they are actually used;
2010-05-25, by wenzelm
renamed HOLCF/Library/ROOT.ML to HOLCF/Library/HOLCF_Library_ROOT.ML to avoid accidental uses of this ML file via the load path -- see also d7711be8c3a9 (obsolete) and ccae4ecd67f4;
2010-05-25, by wenzelm
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
2010-05-25, by wenzelm
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-25, by wenzelm
tuned -- avoid catch-all exception pattern;
2010-05-25, by wenzelm
updated generated files;
2010-05-25, by wenzelm
merged
2010-05-25, by wenzelm
merged
2010-05-24, by webertj
Typo fixed.
2010-05-24, by webertj
move HOLCF/Sum_Cpo.thy to HOLCF/Library
2010-05-24, by huffman
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
2010-05-24, by huffman
move unused pattern match syntax stuff into HOLCF/ex
2010-05-24, by huffman
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
2010-05-24, by huffman
more lemmas
2010-05-24, by haftmann
induction and case rules
2010-05-24, by haftmann
Store registrations in efficient data structure.
2010-05-24, by ballarin
Avoid recomputation of registration instance for lookup.
2010-05-24, by ballarin
Consistently use equality for registration lookup.
2010-05-24, by ballarin
Cleaner implementation of sublocale command.
2010-05-24, by ballarin
Reapply mixin patch: base for performance improvements.
2010-05-24, by ballarin
merged
2010-05-23, by huffman
declare a few more cont2cont rules
2010-05-23, by huffman
HOLCF no longer redefines 'consts' command
2010-05-22, by huffman
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
2010-05-22, by huffman
simplify fixrec continuity tactic
2010-05-22, by huffman
used sledgehammer[isar_proof] to replace slow metis call
2010-05-23, by krauss
Typo fixed.
2010-05-23, by webertj
Typo fixed.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
Improved document structure.
2010-05-23, by webertj
Minor proof tuning.
2010-05-23, by webertj
merged
2010-05-23, by webertj
Refactoring, minor extensions (e.g., church_rosser).
2010-05-23, by webertj
NEWS: removed fixrec_simp attribute
2010-05-22, by huffman
merged
2010-05-22, by huffman
disambiguate some syntax
2010-05-22, by huffman
optimize continuity proofs in fixrec package, using cont2cont rules
2010-05-22, by huffman
add beta_cfun simproc, which uses cont2cont rules
2010-05-22, by huffman
removed fixrec_simp attribute (cf. a2a1c8a658ef)
2010-05-22, by huffman
simplify definition of eta_tac
2010-05-22, by huffman
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
2010-05-22, by huffman
remove cont2cont simproc; instead declare cont2cont rules as simp rules
2010-05-22, by huffman
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
2010-05-22, by huffman
merged
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann
modernized sorting algorithms; quicksort implements sort
2010-05-22, by haftmann
localized properties_for_sort
2010-05-22, by haftmann
@tailrec annotation;
2010-05-24, by wenzelm
renamed "rev" to "reverse" following usual Scala conventions;
2010-05-24, by wenzelm
parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
2010-05-22, by wenzelm
added rev_iterator;
2010-05-22, by wenzelm
tuned;
2010-05-22, by wenzelm
access statically typed dockable windows;
2010-05-22, by wenzelm
simplified dockables using class Dockable;
2010-05-22, by wenzelm
generic dockable window;
2010-05-22, by wenzelm
separate event bus and dockable for raw output (stdout);
2010-05-22, by wenzelm
more Mac OS problems;
2010-05-22, by wenzelm
ignore system messages;
2010-05-22, by wenzelm
use proper ISABELLE_PLATFORM instead of adhoc uname;
2010-05-22, by wenzelm
refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
2010-05-22, by wenzelm
tuned;
2010-05-22, by wenzelm
removed timing;
2010-05-22, by wenzelm
rendering information and style sheets via settings;
2010-05-22, by wenzelm
more brackets -- unaligned to prevent odd auto-indentation;
2010-05-21, by wenzelm
merged
2010-05-21, by wenzelm
adjusted to changes in Mapping.thy
2010-05-21, by haftmann
merged
2010-05-21, by haftmann
tuned
2010-05-21, by haftmann
more lemmas about mappings, in particular keys
2010-05-21, by haftmann
refined
2010-05-21, by haftmann
nats in Haskell are readable
2010-05-21, by haftmann
Let rsp and prs in fun_rel/fun_map format
2010-05-21, by Cezary Kaliszyk
tuned zoom_box;
2010-05-21, by wenzelm
print calculation result in the context where the fact is actually defined -- proper externing;
2010-05-21, by wenzelm
future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
2010-05-21, by wenzelm
some message styling;
2010-05-21, by wenzelm
simplified message markup, using plain XML.Elem directly;
2010-05-21, by wenzelm
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
2010-05-21, by wenzelm
refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
2010-05-21, by wenzelm
bad_result: report fully explicit message;
2010-05-21, by wenzelm
observe additional isabelle-jedit.css for component and user;
2010-05-21, by wenzelm
added checkboxes for debug/tracing filter;
2010-05-21, by wenzelm
more abstract view on prover output messages;
2010-05-21, by wenzelm
added some tooltips;
2010-05-21, by wenzelm
HTML_Panel.handler as overridable method;
2010-05-21, by wenzelm
added Library.undefined (in Scala);
2010-05-21, by wenzelm
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
2010-05-21, by wenzelm
component resize: full handle_resize;
2010-05-21, by wenzelm
speed up some proofs and fix some warnings
2010-05-20, by huffman
merged
2010-05-20, by wenzelm
merged
2010-05-20, by haftmann
proper code generator for complement
2010-05-20, by haftmann
proper document text
2010-05-20, by haftmann
implement Mapping.map_entry
2010-05-20, by haftmann
operations default, map_entry, map_default; more lemmas
2010-05-20, by haftmann
added More_List.thy explicitly
2010-05-20, by haftmann
renamed List_Set to the now more appropriate More_Set
2010-05-20, by haftmann
added theory More_List
2010-05-20, by haftmann
moved generic List operations to theory More_List
2010-05-20, by haftmann
adjusted
2010-05-20, by haftmann
turned old-style mem into an input abbreviation
2010-05-20, by haftmann
zoom font size;
2010-05-20, by wenzelm
added somewhat generic zoom box;
2010-05-20, by wenzelm
try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
2010-05-20, by wenzelm
mutate displayed document synchronously in Swing thread, for improved robustness;
2010-05-20, by wenzelm
read style sheets only once;
2010-05-20, by wenzelm
handle component resize for output / HTML panel;
2010-05-20, by wenzelm
Isabelle_System: allow explicit isabelle_home argument;
2010-05-20, by wenzelm
enable shell script editor mode;
2010-05-20, by wenzelm
merged
2010-05-20, by wenzelm
merged
2010-05-20, by bulwahn
deactivated timing of infering modes
2010-05-20, by bulwahn
adapting examples
2010-05-19, by bulwahn
changing operations for accessing data to work with contexts
2010-05-19, by bulwahn
removed unnecessary Thm.transfer in the predicate compiler
2010-05-19, by bulwahn
changing compilation to work only with contexts; adapting quickcheck
2010-05-19, by bulwahn
removing unused argument in print_modes function
2010-05-19, by bulwahn
moving towards working with proof contexts in the predicate compiler
2010-05-19, by bulwahn
improved values command to handle a special case with tuples and polymorphic predicates more correctly
2010-05-19, by bulwahn
improved behaviour of defined_functions in the predicate compiler
2010-05-19, by bulwahn
move some example files into new HOLCF/Tutorial directory
2010-05-19, by huffman
remove redundant hdvd relation
2010-05-19, by huffman
remove unnecessary constant Fixrec.bind
2010-05-19, by huffman
add section about fixrec definitions with looping simp rules
2010-05-19, by huffman
more informative error message for fixrec when continuity proof fails
2010-05-19, by huffman
determine margin just before rendering -- proper reformatting when updating;
2010-05-20, by wenzelm
simplified alignment via FlowPanel;
2010-05-20, by wenzelm
more systematic treatment of physical document wrt. font size etc.;
2010-05-20, by wenzelm
tuned;
2010-05-20, by wenzelm
general Isabelle_System.try_read;
2010-05-20, by wenzelm
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-20, by wenzelm
inverted "Freeze" to "Follow", which is the default;
2010-05-20, by wenzelm
basic controls to freeze/update prover results;
2010-05-19, by wenzelm
show fully detailed protocol messages;
2010-05-19, by wenzelm
some updates following src/Tools/jEdit/dist-template/settings;
2010-05-19, by wenzelm
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
2010-05-19, by haftmann
merged
2010-05-19, by haftmann
dropped legacy_unconstrainT
2010-05-19, by haftmann
new version of triv_of_class machinery without legacy_unconstrain
2010-05-19, by haftmann
merge
2010-05-19, by haftmann
added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
2010-05-19, by haftmann
remove several redundant lemmas about floor and ceiling
2010-05-18, by huffman
merged
2010-05-18, by huffman
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-17, by huffman
simplify proof
2010-05-17, by huffman
simplify proof
2010-05-17, by huffman
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
2010-05-17, by huffman
prefer structure Keyword and Parse;
2010-05-18, by wenzelm
merged
2010-05-18, by wenzelm
merged
2010-05-17, by huffman
remove simp attribute from square_eq_1_iff
2010-05-17, by huffman
merged
2010-05-17, by blanchet
make sure chained facts don't pop up in the metis proof
2010-05-17, by blanchet
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
2010-05-17, by blanchet
generate proper arity declarations for TFrees for SPASS's DFG format;
2010-05-17, by blanchet
identify common SPASS error more clearly
2010-05-17, by blanchet
remove simp attribute from power2_eq_1_iff
2010-05-17, by huffman
dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-17, by haftmann
dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-17, by haftmann
do not open Legacy by default;
2010-05-18, by wenzelm
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-17, by wenzelm
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-17, by wenzelm
tuned;
2010-05-17, by wenzelm
tuned signature;
2010-05-17, by wenzelm
renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
2010-05-17, by wenzelm
centralized legacy aliases;
2010-05-17, by wenzelm
prefer structure Parse_Spec;
2010-05-16, by wenzelm
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15, by wenzelm
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
2010-05-15, by wenzelm
renamed structure ValueParse to Parse_Value;
2010-05-15, by wenzelm
refer directly to structure Keyword and Parse;
2010-05-15, by wenzelm
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
2010-05-15, by wenzelm
renamed Outer_Parse to Parse (in Scala);
2010-05-15, by wenzelm
renamed Outer_Keyword to Keyword (in Scala);
2010-05-15, by wenzelm
avoid open Conv;
2010-05-15, by wenzelm
less pervasive names from structure Thm;
2010-05-15, by wenzelm
less pervasive names from structure Thm;
2010-05-15, by wenzelm
tuned;
2010-05-15, by wenzelm
merged
2010-05-15, by wenzelm
add real_le_linear to list of legacy theorem names
2010-05-15, by huffman
make SML/NJ happy
2010-05-15, by blanchet
removed unused conversions;
2010-05-15, by wenzelm
tuned header;
2010-05-15, by wenzelm
moved normarith.ML where it is actually used;
2010-05-15, by wenzelm
incorporated further conversions and conversionals, after some minor tuning;
2010-05-15, by wenzelm
eliminated redundant runtime checks;
2010-05-15, by wenzelm
normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
2010-05-15, by krauss
more precise dependencies for HOL-Word-SMT_Examples;
2010-05-15, by wenzelm
merged
2010-05-15, by wenzelm
merge
2010-05-14, by blanchet
added Sledgehammer documentation to TOC
2010-05-14, by blanchet
added some Sledgehammer news
2010-05-14, by blanchet
document Nitpick changes
2010-05-14, by blanchet
merge
2010-05-14, by blanchet
added Sledgehammer manual;
2010-05-14, by blanchet
renamed Sledgehammer options
2010-05-14, by blanchet
renamed options
2010-05-14, by blanchet
remove support for crashing beta solver HaifaSat
2010-05-14, by blanchet
renamed two Sledgehammer options
2010-05-14, by blanchet
merged
2010-05-14, by nipkow
added listsum lemmas
2010-05-14, by nipkow
Revert mixin patch due to inacceptable performance drop.
2010-05-14, by ballarin
add "no_atp"s to Nitpick lemmas
2010-05-14, by blanchet
query _HOME environment variables at run-time, not at build-time
2010-05-14, by blanchet
move Refute dependency from Plain to Main
2010-05-14, by blanchet
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
2010-05-14, by blanchet
recognize new Kodkod error message syntax
2010-05-14, by blanchet
improve precision of set constructs in Nitpick
2010-05-14, by blanchet
produce more potential counterexamples for subset operator (cf. quantifiers)
2010-05-14, by blanchet
improved Sledgehammer proofs
2010-05-14, by blanchet
pass "full_type" argument to proof reconstruction
2010-05-14, by blanchet
made Sledgehammer's full-typed proof reconstruction work for the first time;
2010-05-14, by blanchet
delect installed ATPs dynamically, _not_ at image built time
2010-05-14, by blanchet
Fix syntax; apparently constant apply was introduced in an earlier changeset.
2010-05-13, by ballarin
Merged.
2010-05-13, by ballarin
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
2010-05-13, by ballarin
Remove improper use of mixin in class package.
2010-05-13, by ballarin
Multiset: renamed, added and tuned lemmas;
2010-05-13, by nipkow
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
2010-05-12, by huffman
more precise dependencies
2010-05-13, by boehmes
updated SMT certificates
2010-05-12, by boehmes
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-12, by boehmes
integrated SMT into the HOL image
2010-05-12, by boehmes
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
2010-05-12, by boehmes
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
2010-05-12, by boehmes
split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
2010-05-12, by boehmes
added tracing of reconstruction data
2010-05-12, by boehmes
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
2010-05-12, by boehmes
deleted SMT translation files (to be replaced by a simplified version)
2010-05-12, by boehmes
move the addition of extra facts into a separate module
2010-05-12, by boehmes
normalize numerals: also rewrite Numeral0 into 0
2010-05-12, by boehmes
added missing rewrite rules for natural min and max
2010-05-12, by boehmes
rewrite bool case expressions as if expression
2010-05-12, by boehmes
simplified normalize_rule and moved it further down in the code
2010-05-12, by boehmes
merged addition of rules into one function
2010-05-12, by boehmes
added simplification for distinctness of small lists
2010-05-12, by boehmes
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
2010-05-12, by boehmes
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
2010-05-14, by wenzelm
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
2010-05-13, by wenzelm
the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
2010-05-13, by wenzelm
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
2010-05-13, by wenzelm
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
2010-05-13, by wenzelm
unconstrainT operations on proofs, according to krauss/schropp;
2010-05-13, by wenzelm
added Proofterm.get_name variants according to krauss/schropp;
2010-05-13, by wenzelm
conditional structure SingleAssignment;
2010-05-12, by wenzelm
merged
2010-05-12, by wenzelm
merged
2010-05-12, by haftmann
tuned proofs and fact and class names
2010-05-12, by haftmann
tuned fact collection names and some proofs
2010-05-12, by haftmann
grouped local statements
2010-05-12, by haftmann
tuned test problems
2010-05-12, by haftmann
merged
2010-05-12, by wenzelm
merged
2010-05-12, by nipkow
simplified proof
2010-05-12, by nipkow
modernized specifications;
2010-05-12, by wenzelm
updated/unified some legacy warnings;
2010-05-12, by wenzelm
tuned;
2010-05-12, by wenzelm
do not emit legacy_feature warnings here -- users have no chance to disable them;
2010-05-12, by wenzelm
removed obsolete CVS Ids;
2010-05-12, by wenzelm
removed some obsolete admin stuff;
2010-05-12, by wenzelm
check NEWS;
2010-05-12, by wenzelm
removed obsolete CVS Ids;
2010-05-12, by wenzelm
updated some version numbers;
2010-05-12, by wenzelm
minor tuning;
2010-05-12, by wenzelm
reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
2010-05-12, by wenzelm
merged
2010-05-12, by wenzelm
merged
2010-05-12, by haftmann
modernized specifications; tuned reification
2010-05-12, by haftmann
merged
2010-05-12, by haftmann
added lemmas concerning last, butlast, insort
2010-05-12, by haftmann
Remove RANGE_WARN
2010-05-12, by Cezary Kaliszyk
clarified NEWS entry
2010-05-12, by hoelzl
merged
2010-05-12, by hoelzl
added NEWS entry
2010-05-12, by hoelzl
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
2010-05-11, by hoelzl
Add rules directly to the corresponding class locales instead.
2010-05-11, by hoelzl
Removed usage of normalizating locales.
2010-05-11, by hoelzl
speed up some proofs, fixing linarith_split_limit warnings
2010-05-11, by huffman
fix some linarith_split_limit warnings
2010-05-11, by huffman
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
2010-05-11, by huffman
fix duplicate simp rule warning
2010-05-11, by huffman
no more RealPow.thy (remaining lemmas moved to RealDef.thy)
2010-05-11, by huffman
merged
2010-05-11, by huffman
simplify code for emptiness check
2010-05-11, by huffman
removed lemma real_sq_order; use power2_le_imp_le instead
2010-05-11, by huffman
merged
2010-05-11, by haftmann
merged
2010-05-11, by haftmann
represent de-Bruin indices simply by position in list
2010-05-11, by haftmann
tuned reification functions
2010-05-11, by haftmann
tuned code; toward a tightended interface with generated code
2010-05-11, by haftmann
fix spelling of 'superseded'
2010-05-11, by huffman
NEWS: removed theory PReal
2010-05-11, by huffman
collected NEWS updates for HOLCF
2010-05-11, by huffman
merged
2010-05-11, by huffman
move floor lemmas from RealPow.thy to RComplete.thy
2010-05-11, by huffman
add lemma tendsto_Complex
2010-05-11, by huffman
move some theorems from RealPow.thy to Transcendental.thy
2010-05-11, by huffman
add lemma power2_eq_1_iff; generalize some other lemmas
2010-05-11, by huffman
minimize imports
2010-05-10, by huffman
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
2010-05-10, by huffman
clarified Pretty.font_metrics;
2010-05-12, by wenzelm
format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;
2010-05-12, by wenzelm
tuned;
2010-05-12, by wenzelm
more precise pretty printing based on actual font metrics;
2010-05-11, by wenzelm
predefined spaces;
2010-05-11, by wenzelm
merged
2010-05-11, by wenzelm
support Isabelle plugin properties with defaults;
2010-05-11, by wenzelm
merged
2010-05-11, by Christian Urban
tuned proof so that no simplifier warning is printed
2010-05-11, by Christian Urban
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
2010-05-11, by haftmann
merged
2010-05-11, by haftmann
tuned
2010-05-11, by haftmann
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-05-11, by haftmann
tuned; dropped strange myassoc2
2010-05-10, by haftmann
stylized COOPER exception
2010-05-10, by haftmann
simplified oracle
2010-05-10, by haftmann
shorten names
2010-05-10, by haftmann
updated references to ML files
2010-05-10, by haftmann
only one module fpr presburger method
2010-05-10, by haftmann
moved int induction lemma to theory Int as int_bidirectional_induct
2010-05-10, by haftmann
tuned theory text; dropped unused lemma
2010-05-10, by haftmann
one structure is better than three
2010-05-10, by haftmann
less complex organization of cooper source code
2010-05-10, by haftmann
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
2010-05-10, by haftmann
add real_mult_commute to legacy theorem names
2010-05-10, by huffman
new construction of real numbers using Cauchy sequences
2010-05-10, by huffman
add more credits to ex/Dedekind_Real.thy
2010-05-10, by huffman
put construction of reals using Dedekind cuts in HOL/ex
2010-05-10, by huffman
disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);
2010-05-11, by wenzelm
simple dialogs: ensure Swing thread;
2010-05-10, by wenzelm
font size re-adjustment according to Lobo internals;
2010-05-10, by wenzelm
Scala for Netbeans 6.8v1.1.0rc2;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-05-10, by wenzelm
more convenient look-and-feel setup;
2010-05-10, by wenzelm
more convenient get_font;
2010-05-10, by wenzelm
explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;
2010-05-10, by wenzelm
updated to jedit 4.3.2;
2010-05-10, by wenzelm
ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
2010-05-10, by wenzelm
adapted to scala-2.8.0.RC2;
2010-05-10, by wenzelm
merged
2010-05-10, by wenzelm
real_mult_commute -> mult_commute
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
avoid using real-specific versions of generic lemmas
2010-05-09, by huffman
remove a couple of redundant lemmas; simplify some proofs
2010-05-09, by huffman
merged
2010-05-09, by huffman
add lemmas one_less_inverse and one_le_inverse
2010-05-08, by huffman
do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings
2010-05-09, by krauss
added lemmas rel_comp_UNION_distrib(2)
2010-05-09, by krauss
made SML/NJ happy;
2010-05-08, by wenzelm
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09, by wenzelm
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09, by wenzelm
just one version of Thm.unconstrainT, which affects all variables;
2010-05-09, by wenzelm
added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
2010-05-09, by wenzelm
tuned;
2010-05-09, by wenzelm
removed unused "option" variants of "same" operations;
2010-05-09, by wenzelm
more basic replacement of newlines;
2010-05-09, by wenzelm
static Symbol.spaces;
2010-05-09, by wenzelm
proper use of var stopped;
2010-05-08, by wenzelm
removed junk;
2010-05-08, by wenzelm
tuned headers;
2010-05-08, by wenzelm
tuned;
2010-05-08, by wenzelm
merged
2010-05-08, by wenzelm
merged
2010-05-08, by haftmann
moved normalization proof tool infrastructure to canonical algebraic classes
2010-05-08, by haftmann
added lemmas
2010-05-08, by nipkow
merged
2010-05-08, by haftmann
renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07, by haftmann
delete Groebner_Basis directory -- only one file left
2010-05-07, by haftmann
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-07, by haftmann
merged
2010-05-07, by haftmann
moved lemma zdvd_period to theory Int
2010-05-07, by haftmann
tuned;
2010-05-08, by wenzelm
discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
2010-05-08, by wenzelm
tuned error message: regular Pretty.string_of instead of raw Pretty.output;
2010-05-08, by wenzelm
unified/simplified Pretty.margin_default;
2010-05-08, by wenzelm
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-05-08, by wenzelm
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
2010-05-08, by wenzelm
tuned signature;
2010-05-08, by wenzelm
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08, by wenzelm
back-patching of axclass proofs;
2010-05-08, by wenzelm
back-patching via Single_Assignment.var;
2010-05-08, by wenzelm
support several sidekick parsers -- very basic default parser;
2010-05-07, by wenzelm
sidekick: unformatted content, notably without newlines;
2010-05-07, by wenzelm
unformatted output;
2010-05-07, by wenzelm
output symbolic pretty printing markup and format in the front end;
2010-05-07, by wenzelm
Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version;
2010-05-07, by wenzelm
tuned;
2010-05-07, by wenzelm
strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-07, by wenzelm
use existing undefined function;
2010-05-07, by wenzelm
merged
2010-05-07, by wenzelm
removed semicolons
2010-05-07, by krauss
rule subrelI (for nice Isar proofs of relation inequalities)
2010-05-07, by krauss
merged
2010-05-07, by wenzelm
merged
2010-05-07, by haftmann
prefix normalizing replaces class_semiring
2010-05-07, by haftmann
xsymbolized
2010-05-06, by haftmann
moved method syntax here
2010-05-06, by haftmann
tuned proof
2010-05-06, by haftmann
former free-floating field_comp_conv now in structure Normalizer
2010-05-06, by haftmann
proper sublocales; no free-floating ML sections
2010-05-06, by haftmann
moved some lemmas from Groebner_Basis here
2010-05-06, by haftmann
revert to loose merge semantics
2010-05-06, by haftmann
merged
2010-05-06, by haftmann
moved generic lemmas to appropriate places
2010-05-06, by haftmann
tuned
2010-05-06, by haftmann
dropped duplicate comp_arith
2010-05-06, by haftmann
avoid open; tuned references to theorems
2010-05-06, by haftmann
avoid references to groebner bases in names which have no references to groebner bases
2010-05-06, by haftmann
tuned whitespace
2010-05-06, by haftmann
tuned headings
2010-05-06, by haftmann
avoid open
2010-05-06, by haftmann
tuned internal structure
2010-05-06, by haftmann
fail on merge of conflicting normalization entries: functions are not mergable
2010-05-06, by haftmann
more canonical data administration
2010-05-06, by haftmann
removed former algebra presimpset entirely
2010-05-06, by haftmann
removed former algebra presimpset from accessor
2010-05-06, by haftmann
removed former algebra presimpset from signature
2010-05-06, by haftmann
moved presimplification rules for algebraic methods into named thms functor
2010-05-06, by haftmann
tuned whitespace; dropped superfluous open
2010-05-06, by haftmann
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
2010-05-06, by haftmann
moved nat_arith ot Nat_Numeral: clarified normalizer setup
2010-05-05, by haftmann
dropped unused file
2010-05-05, by haftmann
dropped Id
2010-05-05, by haftmann
remove unused constant preal_of_rat; remove several unused lemmas about preals
2010-05-06, by huffman
respectfullness and preservation of prod_rel
2010-05-06, by Cezary Kaliszyk
ProofContext.init_global
2010-05-06, by haftmann
merged
2010-05-06, by haftmann
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-05, by haftmann
constant name access lattice is not in use any longer
2010-05-06, by haftmann
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
2010-05-06, by wenzelm
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-05-06, by wenzelm
added separate;
2010-05-06, by wenzelm
basic formatting of pretty trees;
2010-05-06, by wenzelm
added content_length;
2010-05-06, by wenzelm
slightly more general Library.chunks;
2010-05-06, by wenzelm
misc tuning -- accumulate body via ListBuffer;
2010-05-06, by wenzelm
basic support for symbolic pretty printing;
2010-05-06, by wenzelm
extractors for document updates;
2010-05-06, by wenzelm
extractors for outer keyword declarations;
2010-05-06, by wenzelm
eliminated deprecated "--" method;
2010-05-05, by wenzelm
use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
2010-05-05, by wenzelm
use SwingApplication instead of deprecated GUIApplication;
2010-05-05, by wenzelm
simplified via Position extractors;
2010-05-05, by wenzelm
some rearrangement of Scala sources;
2010-05-05, by wenzelm
fminus and some more theorems ported from Finite_Set.
2010-05-05, by Cezary Kaliszyk
eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-05, by haftmann
tuned whitespace
2010-05-05, by haftmann
tuned interpunctation, dropped dead comment
2010-05-05, by haftmann
merged
2010-05-04, by huffman
avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)
2010-05-04, by huffman
generalize some lemmas to class t1_space
2010-05-04, by huffman
simplify definition of t1_space; generalize lemma closed_sing and related lemmas
2010-05-04, by huffman
generalize some lemmas
2010-05-04, by huffman
convert comments to 'text' blocks
2010-05-04, by huffman
generalize more lemmas about limits
2010-05-04, by huffman
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
2010-05-05, by krauss
merged
2010-05-04, by huffman
generalize types of LIMSEQ and LIM; generalize many lemmas
2010-05-04, by huffman
make (f -- a --> x) an abbreviation for (f ---> x) (at a)
2010-05-04, by huffman
make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-05-04, by huffman
adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
2010-05-04, by huffman
declare cont_discrete_cpo [cont2cont]
2010-05-04, by huffman
remove unneeded constant Zseq
2010-05-03, by huffman
add lemmas eventually_nhds_metric and tendsto_mono
2010-05-03, by huffman
remove unneeded premise
2010-05-03, by huffman
add constants netmap and nhds
2010-05-03, by huffman
Merged.
2010-05-04, by ballarin
Provide internal function for printing a single interpretation.
2010-05-04, by ballarin
Explicitly manage export in dependencies.
2010-04-27, by ballarin
fixed proof (cf. edc381bf7200);
2010-05-04, by wenzelm
Corrected imports; better approximation of dependencies.
2010-05-04, by hoelzl
Add Convex to Library build
2010-05-04, by hoelzl
Removed unnecessary assumption
2010-05-04, by hoelzl
Translating lemmas from Finite_Set to FSet.
2010-05-04, by Cezary Kaliszyk
merged
2010-05-04, by wenzelm
merged
2010-05-04, by berghofe
Turned Sem into an inductive definition.
2010-05-04, by berghofe
Corrected handling of "for" parameters.
2010-05-04, by berghofe
induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
2010-05-04, by berghofe
added lemma about irreflexivity of pointer inequality in Imperative_HOL
2010-05-04, by bulwahn
added function ffilter and some lemmas from Finite_Set to the FSet theory
2010-05-04, by bulwahn
merged
2010-05-04, by haftmann
avoid if on rhs of default simp rules
2010-05-04, by haftmann
avoid exception Empty on malformed goal
2010-05-04, by krauss
locale predicates of classes carry a mandatory "class" prefix
2010-05-04, by haftmann
a ring_div is a ring_1_no_zero_divisors
2010-05-04, by haftmann
NEWS
2010-05-04, by haftmann
merged
2010-05-03, by huffman
merged
2010-05-01, by huffman
complete_lattice instance for net type
2010-05-01, by huffman
swap ordering on nets, so x <= y means 'x is finer than y'
2010-05-01, by huffman
fixrec no longer uses global simpset internally to prove equations
2010-05-01, by huffman
move setsum lemmas to Product_plus.thy
2010-05-01, by huffman
remove duplicate lemmas
2010-04-30, by huffman
add lemmas about convergent
2010-04-30, by huffman
Cleanup information theory
2010-05-03, by hoelzl
Moved Convex theory to library.
2010-05-03, by hoelzl
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
2010-04-20, by hoelzl
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-05-04, by wenzelm
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-04, by wenzelm
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-05-04, by wenzelm
specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result;
2010-05-04, by wenzelm
UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;
2010-05-03, by wenzelm
replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;
2010-05-03, by wenzelm
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03, by wenzelm
minor tuning of Thm.strip_shyps -- no longer pervasive;
2010-05-03, by wenzelm
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
2010-05-03, by wenzelm
old NEWS on global operations;
2010-05-03, by wenzelm
ProofContext.init_global;
2010-05-03, by wenzelm
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-05-03, by wenzelm
merged
2010-05-03, by haftmann
do not generate code per default -- touches file of parent session
2010-04-30, by haftmann
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-05-01, by krauss
Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
2010-05-01, by krauss
now if this doesn't make SML/NJ happy, nothing will
2010-05-01, by blanchet
more stats;
2010-05-01, by wenzelm
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-04-30, by wenzelm
slightly more standard induct_simp_add/del attributes;
2010-04-30, by wenzelm
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-04-30, by wenzelm
export Simplifier.with_context;
2010-04-30, by wenzelm
removed some old comments;
2010-04-30, by wenzelm
merged
2010-04-30, by huffman
merged
2010-04-30, by huffman
generalize lemma adjoint_unique; simplify some proofs
2010-04-29, by huffman
fix latex url
2010-04-29, by huffman
merged
2010-04-29, by huffman
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-29, by huffman
remove unused function vector_power, unused lemma one_plus_of_nat_neq_0
2010-04-29, by huffman
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
2010-04-29, by huffman
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
2010-04-29, by huffman
generalize LIMSEQ_vector to tendsto_vector
2010-04-28, by huffman
generalize orthogonal_clauses
2010-04-28, by huffman
remove redundant lemma vector_dist_norm
2010-04-28, by huffman
remove redundant lemma norm_0
2010-04-28, by huffman
generalize some euclidean space lemmas
2010-04-28, by huffman
prove lemma openin_subopen without using choice
2010-04-28, by huffman
move path-related stuff into new theory file
2010-04-28, by huffman
add new Multivariate_Analysis files to IsaMakefile
2010-04-28, by huffman
move operator norm stuff to new theory file
2010-04-28, by huffman
eliminated spurious sledgehammer invocation;
2010-04-30, by wenzelm
merged
2010-04-30, by wenzelm
merged
2010-04-30, by haftmann
merged
2010-04-30, by haftmann
enclose case expression in brackets
2010-04-30, by haftmann
catch the right exception
2010-04-30, by blanchet
eliminate trivial case splits from Isar proofs
2010-04-30, by blanchet
remove debugging code
2010-04-30, by blanchet
merged
2010-04-30, by blanchet
minor improvements
2010-04-30, by blanchet
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
2010-04-30, by blanchet
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
2010-04-30, by blanchet
in "overlord" mode: ignore problem prefix specified in the .thy file
2010-04-29, by blanchet
uncomment code
2010-04-29, by blanchet
redid some Sledgehammer/Metis proofs
2010-04-29, by blanchet
fix more "undeclared symbol" errors related to SPASS's DFG format
2010-04-29, by blanchet
be more discriminate: some one-line Isar proofs are silly
2010-04-29, by blanchet
one-step Isar proofs are not always pointless
2010-04-29, by blanchet
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
2010-04-29, by blanchet
redo more Metis/Sledgehammer example
2010-04-29, by blanchet
fixed definition of "bad frees" so that it actually works
2010-04-29, by blanchet
don't remove last line of proof
2010-04-29, by blanchet
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
2010-04-29, by blanchet
make SML/NJ happy, take 2
2010-04-29, by blanchet
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
2010-04-29, by blanchet
expand combinators in Isar proofs constructed by Sledgehammer;
2010-04-29, by blanchet
more neg_clausify proofs that get replaced by direct proofs
2010-04-29, by blanchet
redo some of the metis proofs
2010-04-28, by blanchet
back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
2010-04-28, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip