isabelle: Graph

more robust: avoid NPE due to odd problems with object initialization;
2019-03-25, by wenzelm
RDF meta data for AFP entries;
2019-03-25, by wenzelm
more strict AFP properties;
2019-03-25, by wenzelm
tuned signature;
2019-03-25, by wenzelm
clarified signature;
2019-03-25, by wenzelm
proper treatment of empty extra lines (amending 98a440cfbb2b);
2019-03-25, by wenzelm
clarified signature: explicitly typed interfaces;
2019-03-25, by wenzelm
provide maintainers as seen in AFP/admin;
2019-03-25, by wenzelm
tuned;
2019-03-25, by wenzelm
tuned signature;
2019-03-25, by wenzelm
read AFP metadata for entries;
2019-03-25, by wenzelm
more accurate HTML rendering;
2019-03-24, by wenzelm
clarified markup;
2019-03-24, by wenzelm
clarified rendering, notably of \<^latex>CARTOUCHE in outer syntax;
2019-03-24, by wenzelm
tuned;
2019-03-24, by wenzelm
clarified spell-checking (see also 30233285270a);
2019-03-24, by wenzelm
more accurate markup;
2019-03-24, by wenzelm
clarified signature;
2019-03-24, by wenzelm
more markup for various text kinds, notably for nested formal comments;
2019-03-24, by wenzelm
tuned whitespace;
2019-03-24, by wenzelm
clarified rendering: use COMMENT4 elsewhere;
2019-03-24, by wenzelm
documentation of document markers and re-interpreted command tags;
2019-03-24, by wenzelm
updated to ssh-java-20190323 (with jsch-0.1.55.jar);
2019-03-23, by wenzelm
NEWS for proper Isabelle version;
2019-03-23, by wenzelm
obsolete;
2019-03-23, by wenzelm
proper latex setup;
2019-03-23, by wenzelm
updated docker setup: lib32stdc++6 is no longer required for polyml-5.8, libfontconfig1 is required for headless jdk-11;
2019-03-23, by wenzelm
proper command-line;
2019-03-23, by wenzelm
avoid global .opam directory: shared home leads to confusion about explicit vs. implicit ISABELLE_OCAMLFIND;
2019-03-23, by wenzelm
more explicit opam dependencies;
2019-03-23, by wenzelm
merged
2019-03-22, by wenzelm
clarified GHC and OCaml test setup;
2019-03-22, by wenzelm
updated to cygwin-20190322 -- package required by ocaml_setup for zarith;
2019-03-22, by wenzelm
workaround for the sake of Windows;
2019-03-22, by wenzelm
more robust -- analogous to ocamlfind;
2019-03-22, by wenzelm
even more robust and conservative OCaml setup;
2019-03-22, by wenzelm
executable equality
2019-03-22, by haftmann
improved code equations taken over from AFP
2019-03-22, by haftmann
New abstract topological material
2019-03-22, by paulson
merged
2019-03-21, by nipkow
tuyned
2019-03-21, by nipkow
further robustification (amending 772bdd1ed843);
2019-03-21, by wenzelm
added function
2019-03-21, by nipkow
merged
2019-03-21, by paulson
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
2019-03-21, by paulson
proper ISABELLE_OCAML_VERSION;
2019-03-21, by wenzelm
less ambitious test: lapbroy68 lacks libgmp-dev that is required for ocaml setup of zarith;
2019-03-21, by wenzelm
more robust "switch create";
2019-03-21, by wenzelm
prefer central root: just one copy of this bulky material;
2019-03-21, by wenzelm
updated to current opam-2.0.3, which is also the version provided by Cygwin 3.0.4;
2019-03-21, by wenzelm
updated to cygwin-20190320;
2019-03-20, by wenzelm
updated to Cygwin 3.0.4 (approximation for Isabelle2019);
2019-03-20, by wenzelm
prefer ISABELLE_OCAML_SETUP: Cygwin lacks libzarith;
2019-03-20, by wenzelm
more robust reference to ghc exe (with multi-platform support);
2019-03-20, by wenzelm
more robust: allow empty root (e.g. via symlink);
2019-03-20, by wenzelm
avoid prompt;
2019-03-20, by wenzelm
updated settings: ISABELLE_OCAMLFIND, ISABELLE_OCAML_SETUP, but retain compatibility with historic versions that require ISABELLE_OCAMLC;
2019-03-20, by wenzelm
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
2019-03-20, by wenzelm
proper ISABELLE_HOME (ISABELLE_ROOT is for platform-specific application bootstrap);
2019-03-20, by wenzelm
more robust: allow empty root (e.g. via symlink);
2019-03-20, by wenzelm
merged
2019-03-19, by paulson
new material about topology, etc.; also fixes for yesterday's
2019-03-19, by paulson
merged
2019-03-18, by wenzelm
support unicode_symbols in input source;
2019-03-18, by wenzelm
tuned signature;
2019-03-18, by wenzelm
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
2019-03-18, by paulson
tuned signature;
2019-03-17, by wenzelm
more meta data from "dcterms" (superset of "dc");
2019-03-17, by wenzelm
more latex symbols;
2019-03-15, by wenzelm
merged
2019-03-14, by wenzelm
more specific keyword kinds;
2019-03-14, by wenzelm
tuned whitespace;
2019-03-14, by wenzelm
include zarith in the default opam setup
2019-03-14, by haftmann
dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
2019-03-14, by haftmann
proper theory for type of dual ordered lattice in distribution
2019-03-14, by haftmann
slightly more complete check of code generation for immutable arrays
2019-03-14, by haftmann
CONTRIBUTORS
2019-03-13, by haftmann
migrated from Nums to Zarith as library for OCaml integer arithmetic
2019-03-10, by haftmann
dropped superfluous declaration attribute
2019-03-10, by haftmann
more sanity checks;
2019-03-13, by wenzelm
updated to polyml-5.8 (official release);
2019-03-12, by wenzelm
URIs should normally be "rdf:resource", not string body;
2019-03-11, by wenzelm
clarified signature;
2019-03-11, by wenzelm
support for document meta data in PIDE and RDF;
2019-03-11, by wenzelm
tuned signature;
2019-03-11, by wenzelm
tuned signature;
2019-03-11, by wenzelm
tuned signature;
2019-03-11, by wenzelm
tuned signature;
2019-03-11, by wenzelm
more formal contributors (with the help of the history);
2019-03-10, by wenzelm
proper data columns for plots;
2019-03-10, by wenzelm
merged
2019-03-10, by wenzelm
tuned -- Toplevel.presentation_context is total;
2019-03-10, by wenzelm
document markers are formal comments, and may thus occur anywhere in the command-span;
2019-03-10, by wenzelm
PIDE markup for spell-checking;
2019-03-10, by wenzelm
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
2019-03-10, by wenzelm
tuned;
2019-03-10, by wenzelm
added semantic document markers;
2019-03-10, by wenzelm
clarified signature;
2019-03-09, by wenzelm
added glyph for \<marker>;
2019-03-09, by wenzelm
tuned proof;
2019-03-09, by wenzelm
clarified Toplevel.state: more explicit types;
2019-03-09, by wenzelm
tuned;
2019-03-09, by wenzelm
merged
2019-03-10, by paulson
tidied up HOL/ex/Primrec
2019-03-10, by paulson
proper code_simp setup for literals
2019-03-08, by haftmann
tuned -- more explicit type node_presentation;
2019-03-08, by wenzelm
tuned signature;
2019-03-08, by wenzelm
clarified modules;
2019-03-08, by wenzelm
renamed the constant "limit" as it is too "generic"
2019-03-07, by paulson
new material for Analysis
2019-03-07, by paulson
proper option (amending cc0b3e177b49);
2019-03-06, by wenzelm
removed junk;
2019-03-06, by wenzelm
updated to polyml-5.8-20190306;
2019-03-06, by wenzelm
afford redundant whitespace for improved readability;
2019-03-06, by wenzelm
tuned signature;
2019-03-05, by wenzelm
recover original order;
2019-03-05, by wenzelm
tuned;
2019-03-05, by wenzelm
misc tuning and modernization;
2019-03-05, by wenzelm
merged
2019-03-05, by wenzelm
clarified signature;
2019-03-05, by wenzelm
clarified signature: more general types;
2019-03-05, by wenzelm
afford redundant whitespace for improved readability;
2019-03-05, by wenzelm
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
2019-03-05, by haftmann
tuned signature;
2019-03-03, by wenzelm
clarified signature -- allow more re-use;
2019-03-03, by wenzelm
concrete predicates from "Dublin Core";
2019-03-03, by wenzelm
clarified signature;
2019-03-03, by wenzelm
tuned signature;
2019-03-03, by wenzelm
tuned document;
2019-03-03, by wenzelm
system option "system_heaps" supersedes various command-line options for "system build mode";
2019-03-01, by wenzelm
more uniform session_system_mode (see also e57416b649d5);
2019-03-01, by wenzelm
more implicit reload, similar to VSCode;
2019-03-01, by wenzelm
clarified signature;
2019-03-01, by wenzelm
tuned proofs -- eliminated odd case_tac;
2019-02-28, by wenzelm
more scalable on 32-bit Poly/ML;
2019-02-28, by wenzelm
tuned;
2019-02-28, by wenzelm
more line spacing, notably for ttfautohint (see 4791988fcbc4);
2019-02-27, by wenzelm
more compact representation: approx. factor 2;
2019-02-27, by wenzelm
more scalable on 32-bit Poly/ML;
2019-02-27, by wenzelm
clarified quasi_consolidated status after 5f160df596c1 -- relevant for headless PIDE session (e.g. "isabelle dump");
2019-02-27, by wenzelm
tuned;
2019-02-27, by wenzelm
tuned;
2019-02-25, by wenzelm
clarified signature, notably for hol4isabelle (by Fabian Immler);
2019-02-24, by wenzelm
updated to jedit_build-20190224 (new patches: favorites, glyphvector);
2019-02-24, by wenzelm
fallback on createGlyphVector for multi-character glyphs (e.g. 0x01d49c), as seen in Java 11;
2019-02-24, by wenzelm
formal update of patches -- no change of content;
2019-02-24, by wenzelm
removed junk;
2019-02-24, by wenzelm
merged
2019-02-23, by immler
bundles for floatarith notation
2019-02-23, by immler
merged
2019-02-23, by wenzelm
tuned output;
2019-02-23, by wenzelm
more memory fields;
2019-02-23, by wenzelm
obsolete;
2019-02-23, by wenzelm
no more shadowing of Min and Max by Approximation
2019-02-23, by immler
streamlined specification interfaces
2019-02-21, by haftmann
sligthly more interpunctation and qualification
2019-02-21, by haftmann
tuned whitespace
2019-02-21, by haftmann
physical vs. logical events, the latter takes GC time into account;
2019-02-20, by wenzelm
misc tuning and clarification;
2019-02-20, by wenzelm
misc tuning and clarification;
2019-02-20, by wenzelm
tuned;
2019-02-20, by wenzelm
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
2019-02-20, by wenzelm
dropped junk
2019-02-20, by haftmann
suppress nodes with vacuous status, notably empty nodes (amending 5f160df596c1);
2019-02-18, by wenzelm
tuned;
2019-02-18, by wenzelm
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
2019-02-18, by wenzelm
clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
2019-02-17, by wenzelm
updated to polyml-test-8fda4fd22441;
2019-02-17, by wenzelm
proper installation of ancient procedure for preorders
2019-02-15, by haftmann
CONTRIBUTORS
2019-02-15, by haftmann
more idiomatic style for local declarations in apply scripts
2019-02-15, by haftmann
clarified meta_digest: export_files is a directive for physical output from existing build database;
2019-02-15, by wenzelm
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
2019-02-15, by wenzelm
clarified name;
2019-02-15, by wenzelm
more operations;
2019-02-14, by wenzelm
more operations;
2019-02-14, by wenzelm
support for RDF/XML representation;
2019-02-14, by wenzelm
tuned according to Scala version;
2019-02-14, by wenzelm
support for XML name spaces;
2019-02-14, by wenzelm
uniform XML header;
2019-02-14, by wenzelm
added lemma
2019-02-13, by nipkow
removed subsumed lemma
2019-02-13, by nipkow
too agressive
2019-02-13, by nipkow
added lemmas
2019-02-13, by nipkow
more robust: avoid duplicate Socket.close;
2019-02-10, by wenzelm
enable subpixel anti-aliasing by default, assuming that its 4 variants don't make a difference;
2019-02-10, by wenzelm
updated to isabelle_fonts-20190210;
2019-02-10, by wenzelm
recovered missing glyph;
2019-02-10, by wenzelm
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
2019-02-10, by wenzelm
tuned signature: proper exports;
2019-02-08, by wenzelm
more Haskell operations;
2019-02-08, by wenzelm
Resolved codegen problem with uniformity for formal Laurent series
2019-02-04, by Manuel Eberl
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
2019-02-04, by Manuel Eberl
Exponentiation by squaring, fast modular exponentiation
2019-02-04, by Manuel Eberl
more thorough File.set_executable, notably for Windows;
2019-02-04, by wenzelm
added executable flag for exports;
2019-02-04, by wenzelm
clarified URL -- avoid odd certificate problem with api.media.atlassian.com;
2019-02-04, by wenzelm
back to stable polyml-5.7.1-8 for now;
2019-02-04, by wenzelm
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
2019-02-04, by Manuel Eberl
clarified signature: Path.T as in Generated_Files;
2019-02-02, by wenzelm
back to polyml-test-1b2dcf8f5202 -- more stable;
2019-02-02, by wenzelm
updated to polyml-test-b68438d33c69;
2019-02-01, by wenzelm
clarified default (amending ca9780325a21): it also affects "open-file" dialog, which should be "buffer";
2019-02-01, by wenzelm
NEWS;
2019-01-31, by wenzelm
more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME";
2019-01-31, by wenzelm
merged
2019-01-31, by wenzelm
removed left-over test material (amending bb0a354f6b46);
2019-01-31, by wenzelm
updated to polyml-test-1236652ebd55;
2019-01-31, by wenzelm
added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
2019-01-31, by wenzelm
adapted to a8ee66876a1a;
2019-01-31, by wenzelm
show file-browser favorites more prominently: access to Isabelle resources;
2019-01-31, by wenzelm
tuned -- sort lines;
2019-01-31, by wenzelm
tuned default layout;
2019-01-31, by wenzelm
clarified default layout: global overview left, local document information right;
2019-01-31, by wenzelm
prefer tail-recursive version (despite 4b99b1214034);
2019-01-31, by wenzelm
proper congruence rule for image operator
2019-01-31, by haftmann
less special syntax: make \<Sum> an ordinary function symbol
2019-01-31, by nipkow
more robust: avoid crash of browser right-click menu;
2019-01-30, by wenzelm
more accurate file position;
2019-01-30, by wenzelm
NEWS;
2019-01-30, by wenzelm
open session ROOT file;
2019-01-30, by wenzelm
support for session information via virtual file-system;
2019-01-30, by wenzelm
clarified modules;
2019-01-30, by wenzelm
tuned;
2019-01-30, by wenzelm
tuned signature;
2019-01-30, by wenzelm
tuned signature;
2019-01-30, by wenzelm
tuned;
2019-01-30, by wenzelm
clarified modules;
2019-01-30, by wenzelm
discontinued obsolete option "checkpoint";
2019-01-30, by wenzelm
updated to jdk-11.0.2+9;
2019-01-29, by wenzelm
eliminated suspicious Unicode;
2019-01-29, by wenzelm
eliminated hard TABs;
2019-01-29, by wenzelm
merged
2019-01-29, by nipkow
moved generalized material
2019-01-29, by nipkow
some new results in group theory
2019-01-29, by paulson
less odd class.second_countable_topology_def
2019-01-28, by immler
revert accident with raw Unicode (not Isabelle symbols) in 7404f5b91e56;
2019-01-28, by wenzelm
changed precedence of big operators: now like any other function symbol
2019-01-28, by nipkow
more canonical and less specialized syntax
2019-01-28, by nipkow
updated to polyml-test-1b2dcf8f5202;
2019-01-27, by wenzelm
prefer proper strings in OCaml
2019-01-25, by haftmann
more correct parenthesing
2019-01-25, by haftmann
generalized
2019-01-25, by immler
proper operation in weakly-typed Scala (amending 06153e2e0cdb);
2019-01-25, by wenzelm
tuned
2019-01-25, by nipkow
moved retracts
2019-01-25, by nipkow
tagged 4 theories
2019-01-25, by Angeliki KoutsoukouArgyraki
merged
2019-01-24, by paulson
the theory of Equipollence, and moving Fpow from Cardinals into Main
2019-01-24, by paulson
proper treatment of x86_64_32;
2019-01-24, by wenzelm
more appropriate section
2019-01-24, by haftmann
combinator to lift local theory update to theory update
2019-01-23, by haftmann
merged
2019-01-24, by Angeliki KoutsoukouArgyraki
tagged 5 theories
2019-01-24, by Angeliki KoutsoukouArgyraki
obsolete -- updated in Poly/ML;
2019-01-23, by wenzelm
updated to polyml-test-a444f281ccec;
2019-01-23, by wenzelm
prefer x86_64_32 over x86;
2019-01-23, by wenzelm
clarified signature;
2019-01-23, by wenzelm
updated x86_64-linux base line;
2019-01-23, by wenzelm
fixed me -- indeed this was wrong, as demonstrated by the predicate-free HO output (e.g. ehoh with keep_lams)
2019-01-23, by blanchet
tagged 2 theories ie Cartesian_Euclidean_Space Cartesian_Space
2019-01-23, by Angeliki KoutsoukouArgyraki
minor tagging updates in 13 theories
2019-01-22, by Angeliki KoutsoukouArgyraki
merged
2019-01-22, by Angeliki KoutsoukouArgyraki
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
2019-01-22, by Angeliki KoutsoukouArgyraki
Backed out changeset 1bc422c08209 -- obsolete in AFP/5d11846ac6ab;
2019-01-22, by wenzelm
really keep lambdas in translation if only predicates are missing
2019-01-22, by blanchet
tune ATP settings
2019-01-22, by blanchet
Added triangular numbers
2018-12-14, by Manuel Eberl
keep Local_Theory.reset for now -- still required in many AFP sessions (amending 1c201e4792cb);
2019-01-22, by wenzelm
merged
2019-01-22, by wenzelm
use polyml-test-0a6ebca445fc by default: already quite stable;
2019-01-22, by wenzelm
renamings and new material
2019-01-22, by paulson
merged
2019-01-22, by paulson
some renamings and a bit of new material
2019-01-22, by paulson
slightly more conventional naming schema
2019-01-21, by haftmann
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
2019-01-21, by haftmann
updated news
2019-01-21, by blanchet
get rid of visibility in MaSh -- it slows it down more than it helps
2019-01-21, by blanchet
merged
2019-01-21, by wenzelm
updated polyml platform: 32=x86_64_32;
2019-01-21, by wenzelm
more thorough purge_platforms;
2019-01-21, by wenzelm
clarified ML_OPTIONS on Windows;
2019-01-21, by wenzelm
more operations;
2019-01-21, by wenzelm
new material about summations and powers, along with some tweaks
2019-01-21, by paulson
dedicated combinator for declarations nested in a local theory block
2019-01-20, by haftmann
more conventional parsing of code_stmts antiquotation
2019-01-20, by haftmann
more conventional syntax for code_stmts antiquotation
2019-01-20, by haftmann
avoid crash of jEdit.closeBuffer() via TaskManager.instance.waitForIoTasks() due to race condition of save() vs. automatic load() of already open buffer, e.g. relevant for save-as on "isabelle-export:" artifacts;
2019-01-20, by wenzelm
algebraized more material from theory Divides
2019-01-19, by haftmann
tuned output;
2019-01-19, by wenzelm
more official AFP.groups;
2019-01-19, by wenzelm
auto-update for some experimental components;
2019-01-19, by wenzelm
clarified URLs: prefer sketis over bitbucket;
2019-01-19, by wenzelm
self-contained code modules for Haskell
2019-01-19, by haftmann
automation for unverloading definitions
2019-01-18, by immler
restore type variable names in unoverload_type
2019-01-18, by immler
resolved conflict
2019-01-18, by nipkow
resolved conflict
2019-01-18, by nipkow
tuned headers
2019-01-18, by nipkow
amending 689997a8a582
2019-01-17, by immler
subsection is always %important
2019-01-17, by immler
no need for %unimportant for proofs of proposition
2019-01-17, by immler
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
2019-01-17, by immler
revert to 56acd449da41
2019-01-17, by immler
merge
2019-01-17, by Angeliki KoutsoukouArgyraki
more tagging
2019-01-17, by Angeliki KoutsoukouArgyraki
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
2019-01-16, by Angeliki KoutsoukouArgyraki
chapters for analysis manual
2019-01-16, by immler
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
2019-01-16, by immler
bundle syntax for inner
2019-01-16, by immler
merged
2019-01-16, by wenzelm
tuned;
2019-01-16, by wenzelm
support pruning of export names;
2019-01-16, by wenzelm
clarified signature;
2019-01-16, by wenzelm
Reorg of material
2019-01-16, by nipkow
redundant lemma
2019-01-16, by nipkow
tuned headers
2019-01-16, by nipkow
Reorg of material
2019-01-16, by nipkow
tuned headers
2019-01-16, by nipkow
merged
2019-01-16, by nipkow
moved and renamed class
2019-01-15, by nipkow
added command 'export_generated_files';
2019-01-15, by wenzelm
tuned proofs
2019-01-14, by haftmann
canonical operation to typeset generated code makes dedicated environment obsolete
2019-01-14, by haftmann
tuned
2019-01-14, by haftmann
tuned language
2019-01-14, by haftmann
merged
2019-01-14, by nipkow
tuned
2019-01-14, by nipkow
root_val -> value
2019-01-14, by nipkow
uniform naming
2019-01-14, by nipkow
tagged 5 theories
2019-01-14, by Angeliki KoutsoukouArgyraki
updated tagging first 5
2019-01-14, by Angeliki KoutsoukouArgyraki
more favorites;
2019-01-14, by wenzelm
clarified message;
2019-01-14, by wenzelm
information with hyperlink to "isabelle-export:";
2019-01-13, by wenzelm
support hyperlink to theory exports;
2019-01-13, by wenzelm
regular export with implicit compression: result is uncompressed;
2019-01-13, by wenzelm
clarified -- removed pointless Parse.!!!;
2019-01-13, by wenzelm
tuned;
2019-01-13, by wenzelm
File Browser is open by default;
2019-01-13, by wenzelm
added action "isabelle-export-browser";
2019-01-13, by wenzelm
avoid access to ".NAME.marks" exports;
2019-01-12, by wenzelm
proper _getFile method -- required to open files from browser;
2019-01-12, by wenzelm
more robust: no assumptions about GUI thread or document model;
2019-01-12, by wenzelm
more robust: jEdit may produce names with trailing "/";
2019-01-12, by wenzelm
merged
2019-01-11, by wenzelm
access Isabelle theory exports via virtual file-system;
2019-01-11, by wenzelm
clarified signature;
2019-01-11, by wenzelm
clarified output (again);
2019-01-11, by wenzelm
more operations;
2019-01-11, by wenzelm
tuned signature;
2019-01-11, by wenzelm
tuned
2019-01-11, by nipkow
tuned headers
2019-01-11, by nipkow
clarified output;
2019-01-11, by wenzelm
tuned;
2019-01-11, by wenzelm
export generated files;
2019-01-11, by wenzelm
clarified Path.check_elem;
2019-01-11, by wenzelm
restored test_code for GHC, which got accidentally broken in ef02c5e051e5
2019-01-10, by haftmann
restored quickcheck/narrowing, which got accidentally broken in ef02c5e051e5
2019-01-10, by haftmann
optional code export as theory export
2019-01-10, by haftmann
explicit model concerning files of generated code
2019-01-10, by haftmann
moved generalized lemmas
2019-01-07, by immler
generalized
2019-01-07, by immler
split off Homotopy.thy
2019-01-07, by immler
split off Convex.thy: material that does not require Topology_Euclidean_Space
2019-01-07, by immler
moved setdist to more appropriate places
2019-01-07, by immler
reduced dependencies of Connected.thy
2019-01-07, by immler
split off theory combining Elementary_Topology and Abstract_Topology
2019-01-07, by immler
moved material from Connected.thy to more appropriate places
2019-01-07, by immler
generalized
2019-01-07, by immler
moved material from Connected.thy to more appropriate places
2019-01-07, by immler
generalized
2019-01-07, by immler
moved some material from Connected.thy to more appropriate places
2019-01-06, by immler
proper example for inner syntax, not name;
2019-01-06, by wenzelm
tuned;
2019-01-06, by wenzelm
tuned document layout;
2019-01-06, by wenzelm
retain important whitespace (see 1daf07b65385);
2019-01-06, by wenzelm
merged
2019-01-06, by wenzelm
isabelle update -u path_cartouches;
2019-01-06, by wenzelm
isabelle update -u control_cartouches;
2019-01-06, by wenzelm
support for isabelle update -u path_cartouches;
2019-01-06, by wenzelm
clarified documentation;
2019-01-06, by wenzelm
redundant (see isabelle.Dump.make_options);
2019-01-06, by wenzelm
typed definitions
2019-01-06, by nipkow
documentation on "isabelle update";
2019-01-05, by wenzelm
eliminated spurious \<^print>;
2019-01-05, by wenzelm
isabelle update -u control_cartouches;
2019-01-05, by wenzelm
latex macro for \<^const>;
2019-01-05, by wenzelm
mark for isabelle update -u control_cartouches;
2019-01-05, by wenzelm
proper session base foundations (amending e848328cb2c1);
2019-01-05, by wenzelm
isabelle update -u control_cartouches;
2019-01-04, by wenzelm
support for isabelle update -u control_cartouches;
2019-01-04, by wenzelm
tuned spelling;
2019-01-03, by wenzelm
isabelle update_inner_syntax_cartouches;
2019-01-03, by wenzelm
support for isabelle update -u inner_syntax_cartouches;
2019-01-03, by wenzelm
tuned;
2019-01-03, by wenzelm
isabelle update -u mixfix_cartouches;
2019-01-03, by wenzelm
support for "isabelle update -u mixfix_cartouches";
2019-01-03, by wenzelm
NEWS;
2019-01-03, by wenzelm
tuned signature;
2019-01-03, by wenzelm
tuned output;
2019-01-03, by wenzelm
tuned;
2019-01-03, by wenzelm
tuned;
2019-01-03, by wenzelm
mixfix annotations may use cartouches;
2019-01-03, by wenzelm
tuned;
2019-01-03, by wenzelm
tuned;
2019-01-03, by wenzelm
tuned;
2019-01-03, by wenzelm
tuned signature;
2019-01-03, by wenzelm
clarified signature: more types;
2019-01-03, by wenzelm
tuned;
2019-01-03, by wenzelm
strict bash invocation: proper error checking;
2019-01-02, by wenzelm
more robust system channel via options that are private to the user;
2019-01-02, by wenzelm
tuned messages;
2019-01-02, by wenzelm
merged
2019-01-01, by Andreas Lochbihler
merged
2019-01-01, by Andreas Lochbihler
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
2019-01-01, by Andreas Lochbihler
separate case converter into a separate theory
2018-12-30, by Andreas Lochbihler
more antiquotations -- less LaTeX macros;
2019-01-01, by wenzelm
retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;
2019-01-01, by wenzelm
tuned defs
2019-01-01, by nipkow
merged
2018-12-31, by wenzelm
include loaded_files as doc_blobs (without purging);
2018-12-31, by wenzelm
tuned signature;
2018-12-31, by wenzelm
clarified signature;
2018-12-31, by wenzelm
tuned;
2018-12-31, by wenzelm
tuned;
2018-12-31, by wenzelm
update theory sources based on PIDE markup;
2018-12-31, by wenzelm
clarified signature;
2018-12-31, by wenzelm
dynkin -> Dynkin
2018-12-31, by nipkow
tuned layout
2018-12-31, by nipkow
tuned header
2018-12-31, by nipkow
merged
2018-12-30, by wenzelm
exclude file name components that are special on Windows;
2018-12-30, by wenzelm
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
2018-12-30, by wenzelm
tuned;
2018-12-30, by wenzelm
more strict check: avoid confusion of Path.basic with Path.current / Path.parent;
2018-12-30, by wenzelm
tuned;
2018-12-30, by wenzelm
prefer naming convention from datatype package for strong congruence rules
2018-12-30, by haftmann
redundant
2018-12-30, by haftmann
split off theorems involving classes below metric_space and real_normed_vector
2018-12-29, by immler
merged
2018-12-29, by immler
merged
2018-12-29, by immler
tuned analysis manual
2018-12-29, by immler
tuned signature;
2018-12-29, by wenzelm
merged
2018-12-29, by wenzelm
clarified signature, notably cascade of dump_options, deps, resources, session;
2018-12-29, by wenzelm
unused;
2018-12-29, by wenzelm
clarified signature;
2018-12-29, by wenzelm
clarified errors, according to Isabelle/MMT;
2018-12-29, by wenzelm
tuned, according to Isabelle/MMT;
2018-12-29, by wenzelm
clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress;
2018-12-29, by wenzelm
tuned;
2018-12-29, by wenzelm
merged
2018-12-29, by nipkow
more capitalization
2018-12-29, by nipkow
capitalize proper names in lemma names
2018-12-29, by nipkow
explicit dependencies for includes
2018-12-29, by haftmann
more correct handling of symbols for includes
2018-12-29, by haftmann
more conservative update of Haskell stack (amending 04e54f57a869): 13.0 still lacks notable packages like "Agda" or "darcs";
2018-12-28, by wenzelm
merged;
2018-12-28, by wenzelm
clarified sessions_deps, according to Isabelle/MMT usage;
2018-12-28, by wenzelm
tuned signature: for other dump-like tools;
2018-12-27, by wenzelm
unused;
2018-12-27, by wenzelm
tuned;
2018-12-27, by wenzelm
clarified defaults via system options;
2018-12-27, by wenzelm
added bib-file
2018-12-28, by nipkow
tuned headers etc, added bib-file
2018-12-28, by nipkow
tuned style and headers
2018-12-28, by nipkow
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
2018-12-27, by immler
merged
2018-12-27, by nipkow
tuned headers
2018-12-27, by nipkow
moved lemmas up
2018-12-27, by immler
prove lemmas in context real_normed_vector
2018-12-27, by immler
moved dependency
2018-12-27, by immler
generalized to big sum
2018-12-27, by immler
merged
2018-12-27, by nipkow
tuned headers; ~ -> \<not>
2018-12-27, by nipkow
update LTS Haskell version
2018-12-27, by Lars Hupel
{* verbatim *} is explicit legacy feature;
2018-12-26, by wenzelm
isabelle update_cartouches -t;
2018-12-26, by wenzelm
tuned -- avoid conflict with cartouche argument;
2018-12-26, by wenzelm