src/HOL/ROOT
4 months ago wenzelm 2017-12-07 more robust;
4 months ago wenzelm 2017-12-06 just one session for bulky HOL-Analysis documents;
4 months ago wenzelm 2017-12-03 simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
4 months ago wenzelm 2017-11-27 clarified main sessions;
5 months ago nipkow 2017-11-07 Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
5 months ago wenzelm 2017-11-03 less global theories -- avoid confusion about special cases;
5 months ago wenzelm 2017-11-01 more timing;
5 months ago wenzelm 2017-11-01 build faster without heap images for minor imports;
5 months ago wenzelm 2017-10-31 no censorship (in contrast to 2c828c830ad7);
5 months ago haftmann 2017-10-31 removed ancient nat-int transfer
5 months ago wenzelm 2017-10-30 recovered document from 9bfb6978eb80;
5 months ago wenzelm 2017-10-30 ROOT cleanup: empty 'document_files' means there is no document;
5 months ago wenzelm 2017-10-28 reduced heap hierarchy, for potentially improved performance;
6 months ago wenzelm 2017-10-11 tuned;
6 months ago haftmann 2017-10-08 Polynomial_Factorial does not depend on Field_as_Ring as such
6 months ago haftmann 2017-10-08 removed mere toy example from library
6 months ago wenzelm 2017-10-07 clarified session structure;
6 months ago wenzelm 2017-10-02 prefer file dependencies wrt. specific theories;
6 months ago wenzelm 2017-10-02 proper document (cf. 9f5bfef8bd82);
6 months ago wenzelm 2017-10-02 removed pointless dependencies: done by 'spark_open';
6 months ago wenzelm 2017-10-02 clarified imports: prefer parent session images;
6 months ago wenzelm 2017-10-02 eliminated old-style no-document imports;
7 months ago blanchet 2017-09-08 removed obsolete session
7 months ago nipkow 2017-08-31 Moved material into AFP/Splay_Tree
7 months ago nipkow 2017-08-29 new file
8 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
8 months ago wenzelm 2017-08-17 more complete session (amending e77ea0ea7f2c);
8 months ago wenzelm 2017-08-17 clarified imports;
8 months ago wenzelm 2017-08-17 more complete session (amending 783861a66a60);
8 months ago nipkow 2017-08-15 added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
9 months ago Lars Hupel 2017-07-11 State_Monad ~> Open_State_Syntax
10 months ago wenzelm 2017-06-07 clarified imports;
10 months ago haftmann 2017-06-05 specific output setup is not supposed to intrude regular import theory
10 months ago eberlm 2017-05-29 reorganised material on sublists
11 months ago wenzelm 2017-05-02 more timing;
12 months ago wenzelm 2017-04-24 recovered document from 0f3fdf689bf9;
12 months ago wenzelm 2017-04-24 clarified parent session images, to avoid duplicate loading of theories; avoid name conflict with loaded theory src/HOL/Library/Parallel.thy;
12 months ago wenzelm 2017-04-24 clarified parent session images, to avoid duplicate loading of theories;
12 months ago wenzelm 2017-04-23 actually use theory;
12 months ago wenzelm 2017-04-23 clarified parent session images, to avoid duplicate loading of theories;
12 months ago wenzelm 2017-04-23 actually use theory; tuned;
12 months ago wenzelm 2017-04-23 renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
12 months ago wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
12 months ago wenzelm 2017-04-22 clarified parent session images, to avoid duplicate loading of theories;
12 months ago wenzelm 2017-04-21 tuned;
12 months ago wenzelm 2017-04-21 removed pointless document;
12 months ago wenzelm 2017-04-21 merged
12 months ago wenzelm 2017-04-21 clarified session imports;
12 months ago wenzelm 2017-04-21 tuned imports;
12 months ago wenzelm 2017-04-21 clarified imports;
12 months ago wenzelm 2017-04-21 include imports that morally belong to Main and are used in HOL-Proofs applications;
12 months ago blanchet 2017-04-20 removed Old_SMT legacy module
12 months ago wenzelm 2017-04-19 clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
12 months ago haftmann 2017-04-17 consistent session name
12 months ago wenzelm 2017-04-11 less global theories -- conflict with AFP entries;
12 months ago wenzelm 2017-04-10 explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
12 months ago wenzelm 2017-04-09 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
12 months ago haftmann 2017-04-06 session containing computational algebra
12 months ago haftmann 2017-04-06 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
12 months ago wenzelm 2017-04-04 more main sessions and global theories;