Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
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.
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
unused -- document lacks {* ... *};
2018-12-26, by wenzelm
more rules
2018-12-23, by haftmann
tuned message;
2018-12-23, by wenzelm
tuned messages;
2018-12-22, by wenzelm
more Haskell operations: managed resources for threads;
2018-12-22, by wenzelm
more robust: suitable defaults for unmanaged threads;
2018-12-21, by wenzelm
more Haskell operations;
2018-12-21, by wenzelm
more Haskell operations;
2018-12-21, by wenzelm
proper cleanup;
2018-12-21, by wenzelm
more Haskell operations;
2018-12-21, by wenzelm
clarified;
2018-12-21, by wenzelm
tuned signature;
2018-12-21, by wenzelm
tuned;
2018-12-21, by wenzelm
more Haskell operations;
2018-12-21, by wenzelm
tuned comments;
2018-12-21, by wenzelm
support for File_Format.Session, e.g. server process accessible via prover options;
2018-12-20, by wenzelm
clarified signature;
2018-12-20, by wenzelm
proper trim_line according to ML/Scala versions;
2018-12-20, by wenzelm
proper attach mechanism for any kind of symbols, not just constants
2018-12-20, by haftmann
disregard historic keyword
2018-12-20, by haftmann
more robust open/close bracket, but with potential danger of blocking indefinitely in uninterruptible state;
2018-12-19, by wenzelm
tuned signature;
2018-12-19, by wenzelm
merged
2018-12-19, by wenzelm
tuned;
2018-12-19, by wenzelm
tuned proof text
2018-12-19, by haftmann
tuned proof
2018-12-19, by haftmann
more Isabelle/Haskell operations;
2018-12-18, by wenzelm
clarified signature;
2018-12-16, by wenzelm
tuned comments;
2018-12-16, by wenzelm
tuned -- more compact;
2018-12-16, by wenzelm
more Haskell operations;
2018-12-15, by wenzelm
tuned messages;
2018-12-14, by wenzelm
unused;
2018-12-14, by wenzelm
more ML antiquotations;
2018-12-14, by wenzelm
proper platform path for Windows;
2018-12-14, by wenzelm
tuned whitespace;
2018-12-14, by wenzelm
tuned signature;
2018-12-13, by wenzelm
tuned;
2018-12-13, by wenzelm
clarified UUID operations;
2018-12-13, by wenzelm
clarified protocol;
2018-12-13, by wenzelm
clarified signature;
2018-12-13, by wenzelm
more Haskell operations;
2018-12-13, by wenzelm
tuned signature;
2018-12-13, by wenzelm
clarified signature, e.g. for re-use by other servers;
2018-12-13, by wenzelm
more Haskell operations;
2018-12-13, by wenzelm
clarified modules and signature;
2018-12-13, by wenzelm
tagged more of HOL-Analysis
2018-12-13, by Manuel Eberl
merged;
2018-12-12, by wenzelm
more Haskell operations;
2018-12-12, by wenzelm
more uniform multi-language operations;
2018-12-12, by wenzelm
more Haskell operations;
2018-12-12, by wenzelm
more uniform multi-language operations;
2018-12-12, by wenzelm
more uniform multi-language operations;
2018-12-12, by wenzelm
more operations (as in ML);
2018-12-11, by wenzelm
more uniform multi-language operations;
2018-12-11, by wenzelm
more uniform multi-language operations;
2018-12-11, by wenzelm
Tagged some of HOL-Analysis
2018-12-12, by eberlm
more Haskell operations;
2018-12-10, by wenzelm
tuned headers;
2018-12-10, by wenzelm
more formal Haskell project setup, with dependencies on packages from "stackage";
2018-12-10, by wenzelm
tuned signature;
2018-12-10, by wenzelm
tuned proofs;
2018-12-10, by wenzelm
clarified modules, following bytes.scala;
2018-12-10, by wenzelm
clarified input_line: exclude terminator (its only use in Isabelle_Process.read_command is is unaffected, due to liberal Int.fromString);
2018-12-10, by wenzelm
tuned message;
2018-12-09, by wenzelm
updated to scala-2.12.8;
2018-12-09, by wenzelm
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
2018-12-09, by wenzelm
clarified names;
2018-12-09, by wenzelm
clarified example: avoid unpacking into /home/isabelle/components at TUM;
2018-12-09, by wenzelm
clarified settings and defaults;
2018-12-09, by wenzelm
merged
2018-12-09, by wenzelm
discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
2018-12-08, by wenzelm
clarified defaults for Windows/Cygwin hybrid;
2018-12-08, by wenzelm
proper path before tar -C context switch;
2018-12-08, by wenzelm
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
2018-12-08, by wenzelm
clarified sort order (again, see also 81a75d9a9a4e);
2018-12-08, by wenzelm
clarified operations: uniform sorting of results;
2018-12-08, by wenzelm
clarified modules;
2018-12-08, by wenzelm
clarified gnutar options: more uniform owner;
2018-12-08, by wenzelm
clarified application bundling: discontinued redundant archives;
2018-12-08, by wenzelm
Tagged some theories in HOL-Analysis: Cauchy_Integral_Theorem, Riemann_Mapping and Winding_Numbers.
2018-12-08, by Wenda Li
clarified session dependencies: faster build_doc/build_release;
2018-12-07, by wenzelm
merged
2018-12-07, by paulson
updated to modern symbols
2018-12-07, by paulson
updated to stack-1.9.3;
2018-12-07, by wenzelm
more robust;
2018-12-07, by wenzelm
tuned;
2018-12-07, by wenzelm
obsolete;
2018-12-06, by wenzelm
clarified error;
2018-12-06, by wenzelm
clarified defaults: explicit "rev" takes precedence;
2018-12-06, by wenzelm
more explicit Components.Archive;
2018-12-06, by wenzelm
proper ISABELLE_DOCS_RELEASE_NOTES (amending 39044da8bb5a);
2018-12-06, by wenzelm
tuned message;
2018-12-06, by wenzelm
more explicit Platform.Family;
2018-12-06, by wenzelm
clarified doc sections: add-on components may focus their own application name;
2018-12-06, by wenzelm
more robust, notably for macos /var vs. /private/var;
2018-12-06, by wenzelm
more robust: "gtar" is default name in Homebrew;
2018-12-05, by wenzelm
tuned;
2018-12-05, by wenzelm
more direct File.executable operation: avoid external process (on Unix);
2018-12-05, by wenzelm
clarified absolute isabelle_home and (implicitly) isabelle_home_user;
2018-12-05, by wenzelm
tuned messages;
2018-12-05, by wenzelm
more direct File.link operation: avoid external process;
2018-12-05, by wenzelm
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
2018-12-05, by wenzelm
tuned;
2018-12-04, by wenzelm
updated to jedit_build-20181203 (according to d70767e508d7);
2018-12-03, by wenzelm
Components.download similar to "isabelle components", but without unpacking;
2018-12-03, by wenzelm
clarified signature;
2018-12-03, by wenzelm
clarified signature;
2018-12-03, by wenzelm
more explicit support for Isabelle system components;
2018-12-03, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip