less global theories -- avoid confusion about special cases;
authorwenzelm
Fri Nov 03 13:43:31 2017 +0100 (17 months ago)
changeset 6699269673025292e
parent 66991 fc87d3becd69
child 66993 2c2a346cfe70
less global theories -- avoid confusion about special cases;
src/HOL/Probability/ex/Measure_Not_CCC.thy
src/HOL/ROOT
src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
src/HOL/SPARK/Manual/Complex_Types.thy
src/HOL/SPARK/Manual/Proc1.thy
src/HOL/SPARK/Manual/Proc2.thy
src/HOL/SPARK/Manual/Reference.thy
src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
     1.1 --- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Thu Nov 02 15:21:35 2017 +0100
     1.2 +++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Fri Nov 03 13:43:31 2017 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close>
     1.5  
     1.6  theory Measure_Not_CCC
     1.7 -  imports Probability
     1.8 +  imports "HOL-Probability.Probability"
     1.9  begin
    1.10  
    1.11  text \<open>
     2.1 --- a/src/HOL/ROOT	Thu Nov 02 15:21:35 2017 +0100
     2.2 +++ b/src/HOL/ROOT	Fri Nov 03 13:43:31 2017 +0100
     2.3 @@ -687,7 +687,7 @@
     2.4  
     2.5  session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
     2.6    theories
     2.7 -    Probability (global)
     2.8 +    Probability
     2.9    document_files "root.tex"
    2.10  
    2.11  session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
    2.12 @@ -824,7 +824,7 @@
    2.13  
    2.14  session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
    2.15    theories
    2.16 -    SPARK (global)
    2.17 +    SPARK
    2.18  
    2.19  session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
    2.20    options [spark_prv = false]
     3.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Thu Nov 02 15:21:35 2017 +0100
     3.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Fri Nov 03 13:43:31 2017 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4  *)
     3.5  
     3.6  theory Greatest_Common_Divisor
     3.7 -imports SPARK
     3.8 +imports "HOL-SPARK.SPARK"
     3.9  begin
    3.10  
    3.11  spark_proof_functions
     4.1 --- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Thu Nov 02 15:21:35 2017 +0100
     4.2 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Nov 03 13:43:31 2017 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4  *)
     4.5  
     4.6  theory Longest_Increasing_Subsequence
     4.7 -imports SPARK
     4.8 +imports "HOL-SPARK.SPARK"
     4.9  begin
    4.10  
    4.11  text \<open>
     5.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Thu Nov 02 15:21:35 2017 +0100
     5.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Nov 03 13:43:31 2017 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  *)
     5.5  
     5.6  theory RMD_Specification
     5.7 -imports RMD SPARK
     5.8 +imports RMD "HOL-SPARK.SPARK"
     5.9  begin
    5.10  
    5.11  (* bit operations *)
     6.1 --- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Thu Nov 02 15:21:35 2017 +0100
     6.2 +++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Fri Nov 03 13:43:31 2017 +0100
     6.3 @@ -4,7 +4,7 @@
     6.4  *)
     6.5  
     6.6  theory Sqrt
     6.7 -imports SPARK
     6.8 +imports "HOL-SPARK.SPARK"
     6.9  begin
    6.10  
    6.11  spark_open "sqrt/isqrt"
     7.1 --- a/src/HOL/SPARK/Manual/Complex_Types.thy	Thu Nov 02 15:21:35 2017 +0100
     7.2 +++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Fri Nov 03 13:43:31 2017 +0100
     7.3 @@ -1,5 +1,5 @@
     7.4  theory Complex_Types
     7.5 -imports SPARK
     7.6 +imports "HOL-SPARK.SPARK"
     7.7  begin
     7.8  
     7.9  datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
     8.1 --- a/src/HOL/SPARK/Manual/Proc1.thy	Thu Nov 02 15:21:35 2017 +0100
     8.2 +++ b/src/HOL/SPARK/Manual/Proc1.thy	Fri Nov 03 13:43:31 2017 +0100
     8.3 @@ -1,5 +1,5 @@
     8.4  theory Proc1
     8.5 -imports SPARK
     8.6 +imports "HOL-SPARK.SPARK"
     8.7  begin
     8.8  
     8.9  spark_open "loop_invariant/proc1"
     9.1 --- a/src/HOL/SPARK/Manual/Proc2.thy	Thu Nov 02 15:21:35 2017 +0100
     9.2 +++ b/src/HOL/SPARK/Manual/Proc2.thy	Fri Nov 03 13:43:31 2017 +0100
     9.3 @@ -1,5 +1,5 @@
     9.4  theory Proc2
     9.5 -imports SPARK
     9.6 +imports "HOL-SPARK.SPARK"
     9.7  begin
     9.8  
     9.9  spark_open "loop_invariant/proc2"
    10.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Thu Nov 02 15:21:35 2017 +0100
    10.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Fri Nov 03 13:43:31 2017 +0100
    10.3 @@ -1,6 +1,6 @@
    10.4  (*<*)
    10.5  theory Reference
    10.6 -imports SPARK
    10.7 +imports "HOL-SPARK.SPARK"
    10.8  begin
    10.9  
   10.10  syntax (my_constrain output)
    11.1 --- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Thu Nov 02 15:21:35 2017 +0100
    11.2 +++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Fri Nov 03 13:43:31 2017 +0100
    11.3 @@ -4,7 +4,7 @@
    11.4  *)
    11.5  
    11.6  theory Simple_Greatest_Common_Divisor
    11.7 -imports SPARK
    11.8 +imports "HOL-SPARK.SPARK"
    11.9  begin
   11.10  
   11.11  spark_proof_functions