# 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