proper headers;
authorwenzelm
Mon Mar 16 16:59:59 2015 +0100 (2015-03-16)
changeset 59720f893472fff31
parent 59719 6410a310fdc2
child 59721 5fc2870bd236
child 59723 193f12622072
proper headers;
src/Doc/Logics_ZF/If.thy
src/HOL/Codegenerator_Test/Code_Test_GHC.thy
src/HOL/Codegenerator_Test/Code_Test_MLton.thy
src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
src/HOL/Codegenerator_Test/Code_Test_Scala.thy
src/HOL/Inequalities.thy
src/HOL/Library/Code_Test.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/code_test.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
src/HOL/Tools/Lifting/lifting_bnf.ML
src/Pure/Concurrent/random.ML
src/Pure/GUI/jfx_gui.scala
src/Pure/General/antiquote.scala
src/Pure/General/completion.ML
src/Pure/PIDE/batch_session.scala
src/Pure/System/posix_interrupt.scala
src/Pure/Tools/print_operation.scala
     1.1 --- a/src/Doc/Logics_ZF/If.thy	Mon Mar 16 16:26:33 2015 +0100
     1.2 +++ b/src/Doc/Logics_ZF/If.thy	Mon Mar 16 16:59:59 2015 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Doc/ZF/If.thy
     1.5 +(*  Title:      Doc/Logics_ZF/If.thy
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1991  University of Cambridge
     1.8  
     2.1 --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Mar 16 16:26:33 2015 +0100
     2.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Mon Mar 16 16:59:59 2015 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      Code_Test_GHC.thy
     2.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_GHC.thy
     2.6      Author:     Andreas Lochbihler, ETH Zurich
     2.7  
     2.8  Test case for test_code on GHC
     3.1 --- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Mon Mar 16 16:26:33 2015 +0100
     3.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Mon Mar 16 16:59:59 2015 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      Code_Test_MLtonL.thy
     3.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_MLton.thy
     3.6      Author:     Andreas Lochbihler, ETH Zurich
     3.7  
     3.8  Test case for test_code on MLton
     4.1 --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Mon Mar 16 16:26:33 2015 +0100
     4.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Mon Mar 16 16:59:59 2015 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      Code_Test_OCaml.thy
     4.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_OCaml.thy
     4.6      Author:     Andreas Lochbihler, ETH Zurich
     4.7  
     4.8  Test case for test_code on OCaml
     5.1 --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Mon Mar 16 16:26:33 2015 +0100
     5.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Mon Mar 16 16:59:59 2015 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      Code_Test_PolyML.thy
     5.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_PolyML.thy
     5.6      Author:     Andreas Lochbihler, ETH Zurich
     5.7  
     5.8  Test case for test_code on PolyML
     6.1 --- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Mon Mar 16 16:26:33 2015 +0100
     6.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Mon Mar 16 16:59:59 2015 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      Code_Test_SMLNJ.thy
     6.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
     6.6      Author:     Andreas Lochbihler, ETH Zurich
     6.7  
     6.8  Test case for test_code on SMLNJ
     7.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Mon Mar 16 16:26:33 2015 +0100
     7.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Mon Mar 16 16:59:59 2015 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      Code_Test_Scala.thy
     7.5 +(*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
     7.6      Author:     Andreas Lochbihler, ETH Zurich
     7.7  
     7.8  Test case for test_code on Scala
     8.1 --- a/src/HOL/Inequalities.thy	Mon Mar 16 16:26:33 2015 +0100
     8.2 +++ b/src/HOL/Inequalities.thy	Mon Mar 16 16:59:59 2015 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:     Inequalities
     8.5 +(*  Title:     HOL/Inequalities.thy
     8.6      Author:    Tobias Nipkow
     8.7      Author:    Johannes Hölzl
     8.8  *)
     9.1 --- a/src/HOL/Library/Code_Test.thy	Mon Mar 16 16:26:33 2015 +0100
     9.2 +++ b/src/HOL/Library/Code_Test.thy	Mon Mar 16 16:59:59 2015 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      Code_Test.thy
     9.5 +(*  Title:      HOL/Library/Code_Test.thy
     9.6      Author:     Andreas Lochbihler, ETH Zurich
     9.7  
     9.8  Test infrastructure for the code generator
    10.1 --- a/src/HOL/Library/ContNotDenum.thy	Mon Mar 16 16:26:33 2015 +0100
    10.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Mar 16 16:59:59 2015 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      HOL/Library/ContNonDenum.thy
    10.5 +(*  Title:      HOL/Library/ContNotDenum.thy
    10.6      Author:     Benjamin Porter, Monash University, NICTA, 2005
    10.7      Author:     Johannes Hölzl, TU München
    10.8  *)
    11.1 --- a/src/HOL/Library/code_test.ML	Mon Mar 16 16:26:33 2015 +0100
    11.2 +++ b/src/HOL/Library/code_test.ML	Mon Mar 16 16:59:59 2015 +0100
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      Code_Test.ML
    11.5 +(*  Title:      HOL/Library/code_test.ML
    11.6      Author:     Andreas Lochbihler, ETH Zurich
    11.7  
    11.8  Test infrastructure for the code generator
    12.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Mon Mar 16 16:26:33 2015 +0100
    12.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Mon Mar 16 16:59:59 2015 +0100
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
    12.5 +(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
    12.6      Author:     Nik Sultana, Cambridge University Computer Laboratory
    12.7  
    12.8  Various tests for the proof reconstruction module.
    13.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Mon Mar 16 16:26:33 2015 +0100
    13.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Mon Mar 16 16:59:59 2015 +0100
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
    13.5 +(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
    13.6      Author:     Nik Sultana, Cambridge University Computer Laboratory
    13.7  
    13.8  Unit tests for proof reconstruction module.
    14.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Mar 16 16:26:33 2015 +0100
    14.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Mar 16 16:59:59 2015 +0100
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      HOL/Tools/Transfer/transfer_bnf.ML
    14.5 +(*  Title:      HOL/Tools/Lifting/lifting_bnf.ML
    14.6      Author:     Ondrej Kuncar, TU Muenchen
    14.7  
    14.8  Setup for Lifting for types that are BNF.
    15.1 --- a/src/Pure/Concurrent/random.ML	Mon Mar 16 16:26:33 2015 +0100
    15.2 +++ b/src/Pure/Concurrent/random.ML	Mon Mar 16 16:59:59 2015 +0100
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      Pure/Confurrent/random.ML
    15.5 +(*  Title:      Pure/Concurrent/random.ML
    15.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7  
    15.8  Pseudo random numbers.
    16.1 --- a/src/Pure/GUI/jfx_gui.scala	Mon Mar 16 16:26:33 2015 +0100
    16.2 +++ b/src/Pure/GUI/jfx_gui.scala	Mon Mar 16 16:59:59 2015 +0100
    16.3 @@ -1,4 +1,4 @@
    16.4 -/*  Title:      Pure/GUI/jfx_thread.scala
    16.5 +/*  Title:      Pure/GUI/jfx_gui.scala
    16.6      Module:     PIDE-JFX
    16.7      Author:     Makarius
    16.8  
    17.1 --- a/src/Pure/General/antiquote.scala	Mon Mar 16 16:26:33 2015 +0100
    17.2 +++ b/src/Pure/General/antiquote.scala	Mon Mar 16 16:59:59 2015 +0100
    17.3 @@ -1,4 +1,4 @@
    17.4 -/*  Title:      Pure/ML/antiquote.scala
    17.5 +/*  Title:      Pure/General/antiquote.scala
    17.6      Author:     Makarius
    17.7  
    17.8  Antiquotations within plain text.
    18.1 --- a/src/Pure/General/completion.ML	Mon Mar 16 16:26:33 2015 +0100
    18.2 +++ b/src/Pure/General/completion.ML	Mon Mar 16 16:59:59 2015 +0100
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      Pure/Isar/completion.ML
    18.5 +(*  Title:      Pure/General/completion.ML
    18.6      Author:     Makarius
    18.7  
    18.8  Semantic completion within the formal context.
    19.1 --- a/src/Pure/PIDE/batch_session.scala	Mon Mar 16 16:26:33 2015 +0100
    19.2 +++ b/src/Pure/PIDE/batch_session.scala	Mon Mar 16 16:59:59 2015 +0100
    19.3 @@ -1,4 +1,4 @@
    19.4 -/*  Title:      Pure/Tools/batch_session.scala
    19.5 +/*  Title:      Pure/PIDE/batch_session.scala
    19.6      Author:     Makarius
    19.7  
    19.8  PIDE session in batch mode.
    20.1 --- a/src/Pure/System/posix_interrupt.scala	Mon Mar 16 16:26:33 2015 +0100
    20.2 +++ b/src/Pure/System/posix_interrupt.scala	Mon Mar 16 16:59:59 2015 +0100
    20.3 @@ -1,4 +1,4 @@
    20.4 -/*  Title:      Pure/System/interrupt.scala
    20.5 +/*  Title:      Pure/System/posix_interrupt.scala
    20.6      Author:     Makarius
    20.7  
    20.8  Support for POSIX interrupts (bypassed on Windows).
    21.1 --- a/src/Pure/Tools/print_operation.scala	Mon Mar 16 16:26:33 2015 +0100
    21.2 +++ b/src/Pure/Tools/print_operation.scala	Mon Mar 16 16:59:59 2015 +0100
    21.3 @@ -1,4 +1,4 @@
    21.4 -/*  Title:      Pure/System/print_operation.scala
    21.5 +/*  Title:      Pure/Tools/print_operation.scala
    21.6      Author:     Makarius
    21.7  
    21.8  Print operations as asynchronous query.