# HG changeset patch
# User wenzelm
# Date 1364326652 -3600
# Node ID 8c58fbbc1d5a265c6fb3427a03f71254067aaf9f
# Parent  118f7cb0ee8ed00086f0f4e544004692c6cc7646
tuned session specification;

diff -r 118f7cb0ee8e -r 8c58fbbc1d5a src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 26 20:36:32 2013 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 26 20:37:32 2013 +0100
@@ -8,7 +8,7 @@
   Complex_Main
   "~~/src/HOL/Library/Float"
   "~~/src/HOL/Library/Reflection"
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+  Dense_Linear_Order
   "~~/src/HOL/Library/Code_Target_Numeral"
 begin
 
diff -r 118f7cb0ee8e -r 8c58fbbc1d5a src/HOL/Decision_Procs/Decision_Procs.thy
--- a/src/HOL/Decision_Procs/Decision_Procs.thy	Tue Mar 26 20:36:32 2013 +0100
+++ b/src/HOL/Decision_Procs/Decision_Procs.thy	Tue Mar 26 20:37:32 2013 +0100
@@ -1,11 +1,16 @@
-header {* Various decision procedures, typically involving reflection *}
-
 theory Decision_Procs
 imports
-  Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order
+  Commutative_Ring
+  Cooper
+  Ferrack
+  MIR
+  Approximation
+  Dense_Linear_Order
   Parametric_Ferrante_Rackoff
   Commutative_Ring_Complete
-  "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex"
+  "ex/Commutative_Ring_Ex"
+  "ex/Approximation_Ex"
+  "ex/Dense_Linear_Order_Ex"
 begin
 
 end
diff -r 118f7cb0ee8e -r 8c58fbbc1d5a src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Mar 26 20:36:32 2013 +0100
+++ b/src/HOL/ROOT	Tue Mar 26 20:37:32 2013 +0100
@@ -347,6 +347,9 @@
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Decision_Procs" in Decision_Procs = HOL +
+  description {*
+    Various decision procedures, typically involving reflection.
+  *}
   options [condition = ISABELLE_POLYML, document = false]
   theories Decision_Procs