# HG changeset patch # User wenzelm # Date 1491333100 -7200 # Node ID 35a85aa725e99a60172b9e517a30a77be457ac78 # Parent a5b38d8d3c1e39d451e04d92e76bff9885350ef3 tuned; diff -r a5b38d8d3c1e -r 35a85aa725e9 src/HOL/ROOT --- a/src/HOL/ROOT Tue Apr 04 21:05:07 2017 +0200 +++ b/src/HOL/ROOT Tue Apr 04 21:11:40 2017 +0200 @@ -60,6 +60,17 @@ Refute document_files "root.bib" "root.tex" +session "HOL-Analysis" (main timing) in Analysis = HOL + + theories + Analysis + document_files + "root.tex" + +session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + + theories + Approximations + Circle_Area + session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description {* Author: Gertrud Bauer, TU Munich @@ -709,17 +720,6 @@ theories ATP_Problem_Import -session "HOL-Analysis" (main timing) in Analysis = HOL + - theories - Analysis - document_files - "root.tex" - -session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + - theories - Approximations - Circle_Area - session "HOL-Probability" (timing) in "Probability" = "HOL-Analysis" + theories [document = false] "~~/src/HOL/Library/Countable"