14 months ago paulson 2018-05-08 tidying more messy proofs
14 months ago nipkow 2018-05-08 merged
14 months ago nipkow 2018-05-08 more efficient code
14 months ago wenzelm 2018-05-08 merged
14 months ago wenzelm 2018-05-08 command-line tool "isabelle export"; more documentation; tuned;
14 months ago wenzelm 2018-05-08 more efficient query;
14 months ago wenzelm 2018-05-08 more robust: self-export only;
14 months ago wenzelm 2018-05-08 tuned signature;
14 months ago nipkow 2018-05-08 merged
14 months ago nipkow 2018-05-08 more "sorted" changes
14 months ago nipkow 2018-05-08 more "sorted" changes
14 months ago nipkow 2018-05-08 new def of sorted and sorted_wrt
14 months ago wenzelm 2018-05-07 more operations;
14 months ago wenzelm 2018-05-07 merged
14 months ago wenzelm 2018-05-07 return exports as result for Isabelle server;
14 months ago wenzelm 2018-05-07 more checks;
14 months ago wenzelm 2018-05-07 tuned;
14 months ago wenzelm 2018-05-07 more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure; tuned;
14 months ago wenzelm 2018-05-07 clarified signature; avoid pointless compression;
14 months ago wenzelm 2018-05-07 store exports within PIDE command state; Markup.Export.unapply: proper NAME;
14 months ago haftmann 2018-05-06 removed some lemma duplicates
14 months ago haftmann 2018-05-06 typo
14 months ago haftmann 2018-05-06 more appropriate notion of emptiness
14 months ago paulson 2018-05-06 merged
14 months ago paulson 2018-05-06 more tidying
14 months ago paulson 2018-05-06 starting to tidy up Interval_Integral.thy
14 months ago wenzelm 2018-05-06 more operations;
14 months ago wenzelm 2018-05-06 merged
14 months ago wenzelm 2018-05-06 store exports in session database, with asynchronous / parallel compression;
14 months ago wenzelm 2018-05-06 tuned signature;
14 months ago wenzelm 2018-05-06 tuned signature; clarified modules;
14 months ago wenzelm 2018-05-06 tuned signature;
14 months ago wenzelm 2018-05-05 protocol message for export of theory resources;
14 months ago wenzelm 2018-05-05 hexadecimal representation of byte string;
14 months ago wenzelm 2018-05-05 cleanup session output before starting build job; tuned signature;
14 months ago nipkow 2018-05-06 reinstated old lemma name
14 months ago nipkow 2018-05-06 updated to lemma name change
14 months ago nipkow 2018-05-06 removed asm "finite"
14 months ago wenzelm 2018-05-04 merged
14 months ago wenzelm 2018-05-04 no censorship of view title;
14 months ago wenzelm 2018-05-04 set view title dynamically;
14 months ago nipkow 2018-05-04 tuned
14 months ago nipkow 2018-05-04 tuned
14 months ago paulson 2018-05-03 Some tidying up (mostly regarding summations from 0)
14 months ago paulson 2018-05-03 tidied up Infinite_Products
14 months ago immler 2018-05-03 merged
14 months ago immler 2018-05-03 fixed HOL-Analysis
14 months ago immler 2018-05-03 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
14 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
14 months ago paulson 2018-05-03 a lemma about infinite products
14 months ago paulson 2018-05-02 merged
14 months ago paulson 2018-05-02 tidying up and using real induction methods
14 months ago wenzelm 2018-05-02 tuned -- slightly smaller future closure size;
14 months ago wenzelm 2018-05-02 clarified menu actions;
14 months ago wenzelm 2018-05-02 purge history more thoroughly (see also 3156faac30a7);
14 months ago paulson 2018-05-02 merged
14 months ago paulson 2018-05-02 type class generalisations; some work on infinite products
14 months ago paulson 2018-05-02 merged
14 months ago paulson 2018-05-01 simplified some messy proofs
14 months ago wenzelm 2018-05-01 clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); tuned headers;