2015-06-02 wenzelm 2015-06-02 clarified context;
2015-06-02 wenzelm 2015-06-02 tuned proof;
2015-06-03 noschinl 2015-06-03 merged
2015-06-02 noschinl 2015-06-02 simps_of_case: Better error if split rule is not an equality
2015-06-02 noschinl 2015-06-02 simps_of_case: allow Drule.dummy_thm as ignored split rule
2015-06-01 haftmann 2015-06-01 implicit partial divison operation in integral domains
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-06-01 haftmann 2015-06-01 explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
2015-06-01 haftmann 2015-06-01 dropped dead config option
2015-06-01 haftmann 2015-06-01 tuned, including proper signature for functor argument
2015-06-01 haftmann 2015-06-01 dropped dead code
2015-06-01 haftmann 2015-06-01 explicit argument expansion of uncheck rules; rewriting of user-space type system must behave similarly to abbreviations
2015-06-01 haftmann 2015-06-01 explicit input marker for operations
2015-06-01 haftmann 2015-06-01 completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept
2015-06-01 haftmann 2015-06-01 self-contained formulation of abbrev for named targets
2015-06-01 haftmann 2015-06-01 correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections
2015-06-01 haftmann 2015-06-01 separate function to compute exported abbreviation
2015-06-01 haftmann 2015-06-01 clearly separated target primitives (target_foo) from self-contained target operations (foo)
2015-06-01 haftmann 2015-06-01 tuned order
2015-06-01 haftmann 2015-06-01 dedicated config options to deactivate uncheck phase for improvable syntax
2015-06-01 haftmann 2015-06-01 clarified interfaces for improvable syntax
2015-06-01 haftmann 2015-06-01 tuned
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-06-01 wenzelm 2015-06-01 tuned;
2015-06-01 wenzelm 2015-06-01 discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
2015-06-01 wenzelm 2015-06-01 discontinued legacy;
2015-06-01 wenzelm 2015-06-01 obsolete (see 189c81779a68);
2015-06-01 wenzelm 2015-06-01 eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-06-01 wenzelm 2015-06-01 tuned;
2015-06-01 wenzelm 2015-06-01 clarified context;
2015-06-01 wenzelm 2015-06-01 tuned;
2015-05-31 wenzelm 2015-05-31 obsolete;
2015-05-31 wenzelm 2015-05-31 clarified context;
2015-05-31 wenzelm 2015-05-31 tuned;
2015-05-31 wenzelm 2015-05-31 tuned;
2015-05-30 wenzelm 2015-05-30 standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
2015-05-30 wenzelm 2015-05-30 tuned spelling;
2015-05-30 wenzelm 2015-05-30 unused;
2015-05-30 wenzelm 2015-05-30 tuned;
2015-05-30 wenzelm 2015-05-30 more explicit context;
2015-05-30 wenzelm 2015-05-30 obsolete;
2015-05-30 wenzelm 2015-05-30 tuned -- more direct Thm.renamed_prop;
2015-05-30 wenzelm 2015-05-30 tuned message;
2015-05-30 wenzelm 2015-05-30 tuned whitespace;
2015-05-29 blanchet 2015-05-29 removed model checks from Nitpick
2015-05-29 blanchet 2015-05-29 document Nitpick issue
2015-05-29 paulson 2015-05-29 uncountability: open interval equivalences
2015-05-28 paulson 2015-05-28 Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-28 blanchet 2015-05-28 made Auto Sledgehammer behave more like the real thing
2015-05-28 blanchet 2015-05-28 took out Sledgehammer minimizer optimization that breaks things
2015-05-28 kleing 2015-05-28 modernized (slightly) type compiler in MicroJava
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-05-25 wenzelm 2015-05-25 removed obsolete RC tags;
2015-05-25 wenzelm 2015-05-25 merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
2015-05-25 wenzelm 2015-05-25 Added tag Isabelle2015 for changeset 5ae2a2e74c93
2015-05-23 wenzelm 2015-05-23 clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature; Isabelle2015