# HG changeset patch # User wenzelm # Date 1509713011 -3600 # Node ID 69673025292efe932472a6f8d9f28f1f3d7d27cc # Parent fc87d3becd691e61804aa316f97d944aa3e55366 less global theories -- avoid confusion about special cases; diff -r fc87d3becd69 -r 69673025292e src/HOL/Probability/ex/Measure_Not_CCC.thy --- a/src/HOL/Probability/ex/Measure_Not_CCC.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy Fri Nov 03 13:43:31 2017 +0100 @@ -3,7 +3,7 @@ section \The Category of Measurable Spaces is not Cartesian Closed\ theory Measure_Not_CCC - imports Probability + imports "HOL-Probability.Probability" begin text \ diff -r fc87d3becd69 -r 69673025292e src/HOL/ROOT --- a/src/HOL/ROOT Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/ROOT Fri Nov 03 13:43:31 2017 +0100 @@ -687,7 +687,7 @@ session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + theories - Probability (global) + Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + @@ -824,7 +824,7 @@ session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" + theories - SPARK (global) + SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + options [spark_prv = false] diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Fri Nov 03 13:43:31 2017 +0100 @@ -4,7 +4,7 @@ *) theory Greatest_Common_Divisor -imports SPARK +imports "HOL-SPARK.SPARK" begin spark_proof_functions diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy --- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Fri Nov 03 13:43:31 2017 +0100 @@ -4,7 +4,7 @@ *) theory Longest_Increasing_Subsequence -imports SPARK +imports "HOL-SPARK.SPARK" begin text \ diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Fri Nov 03 13:43:31 2017 +0100 @@ -5,7 +5,7 @@ *) theory RMD_Specification -imports RMD SPARK +imports RMD "HOL-SPARK.SPARK" begin (* bit operations *) diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Examples/Sqrt/Sqrt.thy --- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Fri Nov 03 13:43:31 2017 +0100 @@ -4,7 +4,7 @@ *) theory Sqrt -imports SPARK +imports "HOL-SPARK.SPARK" begin spark_open "sqrt/isqrt" diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Manual/Complex_Types.thy --- a/src/HOL/SPARK/Manual/Complex_Types.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Manual/Complex_Types.thy Fri Nov 03 13:43:31 2017 +0100 @@ -1,5 +1,5 @@ theory Complex_Types -imports SPARK +imports "HOL-SPARK.SPARK" begin datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Manual/Proc1.thy --- a/src/HOL/SPARK/Manual/Proc1.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Manual/Proc1.thy Fri Nov 03 13:43:31 2017 +0100 @@ -1,5 +1,5 @@ theory Proc1 -imports SPARK +imports "HOL-SPARK.SPARK" begin spark_open "loop_invariant/proc1" diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Manual/Proc2.thy --- a/src/HOL/SPARK/Manual/Proc2.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Manual/Proc2.thy Fri Nov 03 13:43:31 2017 +0100 @@ -1,5 +1,5 @@ theory Proc2 -imports SPARK +imports "HOL-SPARK.SPARK" begin spark_open "loop_invariant/proc2" diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Manual/Reference.thy --- a/src/HOL/SPARK/Manual/Reference.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Manual/Reference.thy Fri Nov 03 13:43:31 2017 +0100 @@ -1,6 +1,6 @@ (*<*) theory Reference -imports SPARK +imports "HOL-SPARK.SPARK" begin syntax (my_constrain output) diff -r fc87d3becd69 -r 69673025292e src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy --- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Fri Nov 03 13:43:31 2017 +0100 @@ -4,7 +4,7 @@ *) theory Simple_Greatest_Common_Divisor -imports SPARK +imports "HOL-SPARK.SPARK" begin spark_proof_functions