--- 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
--- 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
--- 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