| 2013-02-16 |
haftmann |
restored proper order of NEWS entries (lost due too long-waiting patches)
|
file |
diff |
annotate
|
| 2013-02-15 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| 2013-02-15 |
blanchet |
updated news
|
file |
diff |
annotate
|
| 2013-02-14 |
haftmann |
consolidation of library theories on product orders
|
file |
diff |
annotate
|
| 2013-02-13 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| 2013-02-10 |
wenzelm |
updated PIDE notes;
|
file |
diff |
annotate
|
| 2013-01-28 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-01-26 |
wenzelm |
clarified NEWS on isabelle build and mkroot;
|
file |
diff |
annotate
|
| 2013-01-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2013-01-31 |
hoelzl |
remove unnecessary assumption from real_normed_vector
|
file |
diff |
annotate
|
| 2013-01-20 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 2013-01-20 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2013-01-20 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2013-01-14 |
kuncar |
NEWS
|
file |
diff |
annotate
|
| 2013-01-11 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2013-01-09 |
wenzelm |
tune spelling;
|
file |
diff |
annotate
|
| 2013-01-08 |
wenzelm |
allow negative argument in "consumes" source format;
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
more reactive completion popup by default;
|
file |
diff |
annotate
|
| 2013-01-04 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2013-01-04 |
wenzelm |
document 'locale_deps';
|
file |
diff |
annotate
|
| 2013-01-03 |
wenzelm |
NEWS: ML runtime statistics;
|
file |
diff |
annotate
|
| 2012-12-31 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2012-12-31 |
wenzelm |
recovered Isabelle2012 NEWS from ae12b92c145a, except for e5420161d11d;
|
file |
diff |
annotate
|
| 2012-12-29 |
nipkow |
new theory Library/Finite_Lattice
|
file |
diff |
annotate
|
| 2012-12-23 |
nipkow |
renamed and added lemmas
|
file |
diff |
annotate
|
| 2012-12-18 |
haftmann |
discontinued legacy antiquotations and styles
|
file |
diff |
annotate
|
| 2012-12-14 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| 2012-12-14 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| 2012-12-14 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2012-12-13 |
Christian Sternagel |
renamed "emb" to "list_hembeq";
|
file |
diff |
annotate
|
| 2012-12-13 |
wenzelm |
smarter handling of tracing messages: prover process pauses and enters user dialog;
|
file |
diff |
annotate
|
| 2012-12-10 |
wenzelm |
more generous tracing limit -- rescaled in MB;
|
file |
diff |
annotate
|
| 2012-12-06 |
wenzelm |
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
|
file |
diff |
annotate
|
| 2012-11-26 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-11-26 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2012-11-26 |
blanchet |
updated NEWS etc.
|
file |
diff |
annotate
|
| 2012-11-26 |
wenzelm |
refined outer syntax 'help' command;
|
file |
diff |
annotate
|
| 2012-11-25 |
wenzelm |
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
|
file |
diff |
annotate
|
| 2012-11-24 |
wenzelm |
more NEWS/CONTRIBUTORS;
|
file |
diff |
annotate
|
| 2012-11-24 |
wenzelm |
improved editing support for control styles;
|
file |
diff |
annotate
|
| 2012-11-24 |
wenzelm |
added ISABELLE_PLATFORM_FAMILY;
|
file |
diff |
annotate
|
| 2012-11-21 |
hoelzl |
NEWS: document changes in HOL-Probability
|
file |
diff |
annotate
|
| 2012-11-21 |
hoelzl |
NEWS (changeset 13211e07d931): add Countable_Set
|
file |
diff |
annotate
|
| 2012-11-21 |
hoelzl |
NEWS (changeset 69b35a75caf3): document changes in FuncSet
|
file |
diff |
annotate
|
| 2012-11-21 |
nipkow |
new theory of immutable arrays
|
file |
diff |
annotate
|
| 2012-11-20 |
wenzelm |
simplified command line of "isabelle install";
|
file |
diff |
annotate
|
| 2012-11-19 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| 2012-11-18 |
wenzelm |
more generous tracing_limit, with explicit system option;
|
file |
diff |
annotate
|
| 2012-11-18 |
wenzelm |
adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
|
file |
diff |
annotate
|
| 2012-11-17 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2012-11-08 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-11-06 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| 2012-10-22 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
| 2012-10-22 |
wenzelm |
more detailed Prover IDE NEWS;
|
file |
diff |
annotate
|
| 2012-10-21 |
webertj |
merged
|
file |
diff |
annotate
|
| 2012-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| 2012-10-20 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| 2012-10-18 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
| 2012-10-16 |
wenzelm |
support for more informative errors in lazy enumerations;
|
file |
diff |
annotate
|
| 2012-10-12 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2012-10-12 |
wenzelm |
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
|
file |
diff |
annotate
|
| 2012-10-11 |
haftmann |
simplified construction of fold combinator on multisets;
|
file |
diff |
annotate
|
| 2012-10-10 |
Andreas Lochbihler |
efficient construction of red black trees from sorted associative lists
|
file |
diff |
annotate
|
| 2012-10-08 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
| 2012-10-08 |
haftmann |
corrected NEWS
|
file |
diff |
annotate
|
| 2012-10-04 |
wenzelm |
some documentation of show_markup;
|
file |
diff |
annotate
|
| 2012-09-28 |
wenzelm |
smarter handling of tracing messages;
|
file |
diff |
annotate
|
| 2012-09-22 |
wenzelm |
some PIDE NEWS from this summer;
|
file |
diff |
annotate
|
| 2012-09-21 |
blanchet |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file |
diff |
annotate
|
| 2012-09-20 |
Andreas Lochbihler |
NEWS and CONTRIBUTORS for a5377f6d9f14 and f0ecc1550998
|
file |
diff |
annotate
|
| 2012-09-15 |
haftmann |
typeclass formalising bounded subtraction
|
file |
diff |
annotate
|
| 2012-09-14 |
blanchet |
merged two commands
|
file |
diff |
annotate
|
| 2012-09-12 |
blanchet |
renamed "Ordinals_and_Cardinals" to "Cardinals"
|
file |
diff |
annotate
|
| 2012-09-10 |
wenzelm |
more explicit indication of legacy features;
|
file |
diff |
annotate
|
| 2012-09-07 |
haftmann |
lattice instances for option type
|
file |
diff |
annotate
|
| 2012-09-07 |
haftmann |
combinator Option.these
|
file |
diff |
annotate
|
| 2012-09-04 |
Christian Sternagel |
NEWS; CONTRIBUTORS
|
file |
diff |
annotate
|
| 2012-09-03 |
wenzelm |
"isabelle logo" produces EPS and PDF format simultaneously;
|
file |
diff |
annotate
|
| 2012-08-29 |
wenzelm |
provide polyml-5.4.1 as regular component;
|
file |
diff |
annotate
|
| 2012-08-29 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| 2012-08-28 |
blanchet |
updated NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2012-08-27 |
wenzelm |
clarified "isabelle logo";
|
file |
diff |
annotate
|
| 2012-08-22 |
wenzelm |
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
|
file |
diff |
annotate
|
| 2012-08-17 |
wenzelm |
some explanations on isabelle components;
|
file |
diff |
annotate
|
| 2012-08-14 |
wenzelm |
support for 'typ' with explicit sort constraint;
|
file |
diff |
annotate
|
| 2012-08-08 |
wenzelm |
discontinued obsolete "isabelle makeall";
|
file |
diff |
annotate
|
| 2012-08-07 |
wenzelm |
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
|
file |
diff |
annotate
|
| 2012-08-06 |
wenzelm |
"isabelle options" prints Isabelle system options;
|
file |
diff |
annotate
|
| 2012-08-05 |
wenzelm |
more on isabelle mkroot;
|
file |
diff |
annotate
|
| 2012-08-03 |
wenzelm |
simplified custom document/build script, instead of old-style document/IsaMakefile;
|
file |
diff |
annotate
|
| 2012-07-31 |
wenzelm |
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
|
file |
diff |
annotate
|
| 2012-07-28 |
wenzelm |
discontinued obsolete Isabelle/build script;
|
file |
diff |
annotate
|
| 2012-07-28 |
wenzelm |
announce advanced support for Isabelle sessions and build management;
|
file |
diff |
annotate
|
| 2012-07-28 |
wenzelm |
discontinued special treatment of Proof General;
|
file |
diff |
annotate
|
| 2012-07-23 |
haftmann |
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
|
file |
diff |
annotate
|
| 2012-07-22 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2012-07-20 |
blanchet |
added MaSh to news
|
file |
diff |
annotate
|
| 2012-07-19 |
haftmann |
export code relatively to master directory
|
file |
diff |
annotate
|
| 2012-07-18 |
blanchet |
removed lie
|
file |
diff |
annotate
|
| 2012-07-18 |
blanchet |
doc updates
|
file |
diff |
annotate
|
| 2012-07-06 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-07-06 |
wenzelm |
discontinued obsolete attribute "COMP";
|
file |
diff |
annotate
|
| 2012-06-29 |
wenzelm |
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
|
file |
diff |
annotate
|
| 2012-06-25 |
wenzelm |
updated "isar-ref" manual, reduced remaining material in "ref" manual.
|
file |
diff |
annotate
|
| 2012-06-21 |
bulwahn |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2012-06-06 |
blanchet |
updated NEWS
|
file |
diff |
annotate
|
| 2012-06-04 |
boehmes |
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
|
file |
diff |
annotate
|
| 2012-05-29 |
bulwahn |
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
|
file |
diff |
annotate
|
| 2012-05-24 |
wenzelm |
discontinued support for Poly/ML 5.2.1;
|
file |
diff |
annotate
|
| 2012-05-23 |
wenzelm |
discontinued obsolete method fastsimp / tactic fast_simp_tac;
|
file |
diff |
annotate
|
| 2012-05-23 |
wenzelm |
merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;
|
file |
diff |
annotate
|
| 2012-05-02 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 2012-05-03 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2012-05-02 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| 2012-05-02 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| 2012-05-02 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| 2012-05-02 |
huffman |
edit NEWS items for transfer/lifting
|
file |
diff |
annotate
|
| 2012-04-30 |
Gerwin Klein |
provide [[record_codegen]] option for skipping codegen setup for records
|
file |
diff |
annotate
|
| 2012-04-28 |
wenzelm |
some re-ordering;
|
file |
diff |
annotate
|
| 2012-04-28 |
wenzelm |
updated system manual for release;
|
file |
diff |
annotate
|
| 2012-04-28 |
haftmann |
less confusion in NEWS
|
file |
diff |
annotate
|
| 2012-04-27 |
wenzelm |
mention tools and packages earlier;
|
file |
diff |
annotate
|
| 2012-04-27 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-04-27 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-04-25 |
hoelzl |
sorted lemma list in NEWS
|
file |
diff |
annotate
|
| 2012-04-23 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2012-04-23 |
krauss |
NEWS
|
file |
diff |
annotate
|
| 2012-04-23 |
wenzelm |
typedef with implicit set definition is considered legacy;
|
file |
diff |
annotate
|
| 2012-04-23 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| 2012-04-22 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2012-04-22 |
blanchet |
fixed typos
|
file |
diff |
annotate
|
| 2012-04-22 |
wenzelm |
USER_HOME settings variable points to cross-platform user home directory;
|
file |
diff |
annotate
|
| 2012-04-21 |
huffman |
update NEWS for transfer/quotient
|
file |
diff |
annotate
|
| 2012-04-21 |
huffman |
NEWS for transfer, lifting, and quotient
|
file |
diff |
annotate
|
| 2012-04-20 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| 2012-04-19 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2012-04-19 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| 2012-04-19 |
wenzelm |
more robust Sledgehammer in Prover IDE;
|
file |
diff |
annotate
|
| 2012-04-17 |
Thomas Sewell |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file |
diff |
annotate
|
| 2012-04-18 |
blanchet |
Sledgehammer NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2012-04-18 |
haftmann |
dropped errorneous NEWS entry
|
file |
diff |
annotate
|
| 2012-04-18 |
haftmann |
consolidated NEWS entries on fold
|
file |
diff |
annotate
|
| 2012-04-18 |
haftmann |
grouped fold-related NEWS entries together
|
file |
diff |
annotate
|
| 2012-04-18 |
haftmann |
grouped NEWS concerning relations together
|
file |
diff |
annotate
|
| 2012-04-18 |
haftmann |
merged rename traces
|
file |
diff |
annotate
|
| 2012-04-16 |
wenzelm |
repaired some damage caused by merging with version from 12 days ago (cf. 8c8f27864ed1);
|
file |
diff |
annotate
|
| 2012-04-16 |
nipkow |
merged
|
file |
diff |
annotate
|
| 2012-04-04 |
nipkow |
refined new tutorial announcement
|
file |
diff |
annotate
|
| 2012-04-15 |
wenzelm |
some coverage of bundled declarations;
|
file |
diff |
annotate
|
| 2012-04-15 |
wenzelm |
some coverage of unnamed contexts, which can be nested within other targets;
|
file |
diff |
annotate
|
| 2012-04-14 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2012-04-14 |
wenzelm |
revert changes of already published NEWS;
|
file |
diff |
annotate
|
| 2012-04-14 |
wenzelm |
some updates for release;
|
file |
diff |
annotate
|
| 2012-04-14 |
wenzelm |
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
|
file |
diff |
annotate
|
| 2012-04-13 |
Andreas Lochbihler |
Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
file |
diff |
annotate
|
| 2012-04-13 |
Andreas Lochbihler |
NEWS
|
file |
diff |
annotate
|
| 2012-04-13 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-04-11 |
wenzelm |
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
|
file |
diff |
annotate
|
| 2012-04-10 |
wenzelm |
some coverage of HOL/TPTP;
|
file |
diff |
annotate
|
| 2012-04-06 |
haftmann |
abandoned almost redundant *_foldr lemmas
|
file |
diff |
annotate
|
| 2012-04-06 |
haftmann |
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
|
file |
diff |
annotate
|
| 2012-04-04 |
bulwahn |
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
|
file |
diff |
annotate
|
| 2012-04-02 |
nipkow |
new tutorial
|
file |
diff |
annotate
|
| 2012-04-01 |
krauss |
less modest NEWS; CONTRIBUTORS
|
file |
diff |
annotate
|
| 2012-04-01 |
krauss |
renamed import session back to Import, conforming to directory name; NEWS
|
file |
diff |
annotate
|
| 2012-03-30 |
huffman |
removed redundant nat-specific copies of theorems
|
file |
diff |
annotate
|
| 2012-03-30 |
haftmann |
power on predicate relations
|
file |
diff |
annotate
|
| 2012-03-29 |
bulwahn |
announcing NEWS (cf. 446cfc760ccf)
|
file |
diff |
annotate
|
| 2012-03-28 |
wenzelm |
clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME;
|
file |
diff |
annotate
|
| 2012-03-28 |
huffman |
merged
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove more redundant lemmas
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
generalized lemma zpower_zmod
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
generalize more div/mod lemmas
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
generalize some theorems about div/mod
|
file |
diff |
annotate
|
| 2012-03-27 |
wenzelm |
updated to jedit-4.5.1;
|
file |
diff |
annotate
|
| 2012-03-27 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| 2012-03-24 |
wenzelm |
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
|
file |
diff |
annotate
|
| 2012-03-25 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| 2012-03-22 |
haftmann |
more instructive NEWS
|
file |
diff |
annotate
|
| 2012-03-17 |
wenzelm |
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
|
file |
diff |
annotate
|
| 2012-03-17 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| 2012-03-17 |
haftmann |
generalized INF_INT_eq, SUP_UN_eq
|
file |
diff |
annotate
|
| 2012-03-17 |
wenzelm |
'definition' no longer exports the foundational "raw_def";
|
file |
diff |
annotate
|
| 2012-03-16 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2012-03-16 |
paulson |
ZF news
|
file |
diff |
annotate
|
| 2012-03-16 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| 2012-03-16 |
wenzelm |
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
|
file |
diff |
annotate
|
| 2012-03-15 |
wenzelm |
Isabelle/jEdit supports user-defined Isar commands within the running session;
|
file |
diff |
annotate
|
| 2012-03-15 |
wenzelm |
added ML antiquotation @{keyword};
|
file |
diff |
annotate
|
| 2012-03-14 |
wenzelm |
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
|
file |
diff |
annotate
|
| 2012-03-13 |
wenzelm |
improved attribute "abs_def" to handle object-equality as well;
|
file |
diff |
annotate
|
| 2012-03-12 |
noschinl |
NEWS
|
file |
diff |
annotate
|
| 2012-03-07 |
haftmann |
less rigorous but more realistic migration recommendation; note on code generation of sets
|
file |
diff |
annotate
|
| 2012-03-01 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| 2012-02-28 |
blanchet |
spelling
|
file |
diff |
annotate
|
| 2012-02-24 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| 2012-02-22 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-02-18 |
krauss |
NEWS
|
file |
diff |
annotate
|
| 2012-02-17 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| 2012-02-16 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
discontinued obsolete "prems" fact;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| 2012-02-15 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| 2012-02-14 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2012-02-04 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
| 2012-01-31 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2012-01-30 |
blanchet |
docs and news
|
file |
diff |
annotate
|
| 2012-01-30 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-01-19 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
| 2012-01-17 |
bulwahn |
refreshing NEWS
|
file |
diff |
annotate
|
| 2012-01-16 |
wenzelm |
position constraints for numerals enable PIDE markup;
|
file |
diff |
annotate
|
| 2012-01-10 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2012-01-09 |
wenzelm |
misc tuning and reformatting;
|
file |
diff |
annotate
|
| 2012-01-06 |
haftmann |
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
|
file |
diff |
annotate
|
| 2012-01-06 |
haftmann |
more explicit NEWS
|
file |
diff |
annotate
|
| 2012-01-06 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
|
file |
diff |
annotate
|
| 2012-01-05 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file |
diff |
annotate
|
| 2012-01-05 |
wenzelm |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
| 2011-12-29 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
| 2011-12-28 |
huffman |
fix typos
|
file |
diff |
annotate
|
| 2011-12-28 |
huffman |
remove some duplicate lemmas
|
file |
diff |
annotate
|
| 2011-12-27 |
haftmann |
be explicit about Finite_Set.fold
|
file |
diff |
annotate
|
| 2011-12-26 |
haftmann |
NEWS: unavoidable fact renames
|
file |
diff |
annotate
|
| 2011-12-24 |
haftmann |
NEWS: `set` is now a proper type constructor
|
file |
diff |
annotate
|
| 2011-12-23 |
huffman |
remove redundant lemma word_sub_def
|
file |
diff |
annotate
|
| 2011-12-21 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-12-14 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-12-13 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
| 2011-12-10 |
huffman |
prove class instances without extra lemmas
|
file |
diff |
annotate
|
| 2011-12-09 |
huffman |
remove redundant lemma word_diff_minus
|
file |
diff |
annotate
|
| 2011-12-09 |
noschinl |
more systematic lemma name
|
file |
diff |
annotate
|
| 2011-12-05 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-12-04 |
huffman |
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
|
file |
diff |
annotate
|
| 2011-12-01 |
blanchet |
added "minimize" option for more control over automatic minimization
|
file |
diff |
annotate
|