updated headers;
authorwenzelm
Sun Oct 02 14:07:43 2016 +0200 (2016-10-02)
changeset 639923aa9837d05c7
parent 63991 0d8cd1f3c26d
child 63993 9c0ff0c12116
updated headers;
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Summation_Tests.thy
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/Probability/Characteristic_Functions.thy
src/HOL/Probability/Distribution_Functions.thy
src/HOL/Tools/Argo/argo_real.ML
src/HOL/Tools/Argo/argo_sat_solver.ML
src/HOL/Tools/Argo/argo_tactic.ML
src/Pure/General/json.scala
src/Pure/Tools/ci_api.scala
src/Tools/Argo/argo_expr.ML
src/Tools/Argo/argo_thy.ML
     1.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Oct 02 13:47:39 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Sun Oct 02 14:07:43 2016 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Analysis/Extension.thy
     1.5 +(*  Title:      HOL/Analysis/Continuous_Extension.thy
     1.6      Authors:    LC Paulson, based on material from HOL Light
     1.7  *)
     1.8  
     2.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Sun Oct 02 13:47:39 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Sun Oct 02 14:07:43 2016 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:    HOL/Analysis/Gamma.thy
     2.5 +(*  Title:    HOL/Analysis/Gamma_Function.thy
     2.6      Author:   Manuel Eberl, TU München
     2.7  *)
     2.8  
     3.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Sun Oct 02 13:47:39 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Sun Oct 02 14:07:43 2016 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:    HOL/Analysis/Summation.thy
     3.5 +(*  Title:    HOL/Analysis/Summation_Tests.thy
     3.6      Author:   Manuel Eberl, TU München
     3.7  *)
     3.8  
     4.1 --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Oct 02 13:47:39 2016 +0200
     4.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Oct 02 14:07:43 2016 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Library/Predicate_Compile_Alternative_Defs.thy
     4.5 +(*  Title:      HOL/Library/Predicate_Compile_Quickcheck.thy
     4.6      Author:     Lukas Bulwahn, TU Muenchen
     4.7  *)
     4.8  
     5.1 --- a/src/HOL/Probability/Characteristic_Functions.thy	Sun Oct 02 13:47:39 2016 +0200
     5.2 +++ b/src/HOL/Probability/Characteristic_Functions.thy	Sun Oct 02 14:07:43 2016 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:     Characteristic_Functions.thy
     5.5 +(*  Title:     HOL/Probability/Characteristic_Functions.thy
     5.6      Authors:   Jeremy Avigad (CMU), Luke Serafin (CMU), Johannes Hölzl (TUM)
     5.7  *)
     5.8  
     6.1 --- a/src/HOL/Probability/Distribution_Functions.thy	Sun Oct 02 13:47:39 2016 +0200
     6.2 +++ b/src/HOL/Probability/Distribution_Functions.thy	Sun Oct 02 14:07:43 2016 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:    Distribution_Functions.thy
     6.5 +(*  Title:    HOL/Probability/Distribution_Functions.thy
     6.6      Authors:  Jeremy Avigad (CMU) and Luke Serafin (CMU)
     6.7  *)
     6.8  
     7.1 --- a/src/HOL/Tools/Argo/argo_real.ML	Sun Oct 02 13:47:39 2016 +0200
     7.2 +++ b/src/HOL/Tools/Argo/argo_real.ML	Sun Oct 02 14:07:43 2016 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/Tools/argo_real.ML
     7.5 +(*  Title:      HOL/Tools/Argo/argo_real.ML
     7.6      Author:     Sascha Boehme
     7.7  
     7.8  Extension of the Argo tactic for the reals.
     8.1 --- a/src/HOL/Tools/Argo/argo_sat_solver.ML	Sun Oct 02 13:47:39 2016 +0200
     8.2 +++ b/src/HOL/Tools/Argo/argo_sat_solver.ML	Sun Oct 02 14:07:43 2016 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Tools/argo_sat_solver.ML
     8.5 +(*  Title:      HOL/Tools/Argo/argo_sat_solver.ML
     8.6      Author:     Sascha Boehme
     8.7  
     8.8  A SAT solver based on the Argo solver.
     9.1 --- a/src/HOL/Tools/Argo/argo_tactic.ML	Sun Oct 02 13:47:39 2016 +0200
     9.2 +++ b/src/HOL/Tools/Argo/argo_tactic.ML	Sun Oct 02 14:07:43 2016 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/Tools/argo_tactic.ML
     9.5 +(*  Title:      HOL/Tools/Argo/argo_tactic.ML
     9.6      Author:     Sascha Boehme
     9.7  
     9.8  HOL method and tactic for the Argo solver.
    10.1 --- a/src/Pure/General/json.scala	Sun Oct 02 13:47:39 2016 +0200
    10.2 +++ b/src/Pure/General/json.scala	Sun Oct 02 14:07:43 2016 +0200
    10.3 @@ -1,4 +1,4 @@
    10.4 -/*  Title:      Pure/Tools/json.scala
    10.5 +/*  Title:      Pure/General/json.scala
    10.6      Author:     Makarius
    10.7  
    10.8  Support for JSON parsing.
    11.1 --- a/src/Pure/Tools/ci_api.scala	Sun Oct 02 13:47:39 2016 +0200
    11.2 +++ b/src/Pure/Tools/ci_api.scala	Sun Oct 02 14:07:43 2016 +0200
    11.3 @@ -1,4 +1,4 @@
    11.4 -/*  Title:      Pure/Tools/build.scala
    11.5 +/*  Title:      Pure/Tools/ci_api.scala
    11.6      Author:     Makarius
    11.7  
    11.8  API for Isabelle Jenkins continuous integration services.
    12.1 --- a/src/Tools/Argo/argo_expr.ML	Sun Oct 02 13:47:39 2016 +0200
    12.2 +++ b/src/Tools/Argo/argo_expr.ML	Sun Oct 02 14:07:43 2016 +0200
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      Tools/Argo/sid_expr.ML
    12.5 +(*  Title:      Tools/Argo/argo_expr.ML
    12.6      Author:     Sascha Boehme
    12.7  
    12.8  The input language of the Argo solver.
    13.1 --- a/src/Tools/Argo/argo_thy.ML	Sun Oct 02 13:47:39 2016 +0200
    13.2 +++ b/src/Tools/Argo/argo_thy.ML	Sun Oct 02 14:07:43 2016 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      Tools/Argo/argo_theory.ML
    13.5 +(*  Title:      Tools/Argo/argo_thy.ML
    13.6      Author:     Sascha Boehme
    13.7  
    13.8  Combination of all theory solvers.