isabelle: Graph

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