adjusted comments
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55061a0adf838e2d1
parent 55060 3105434fb02f
child 55062 6d3fad6f01c9
adjusted comments
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_gfp_util.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_util.ML
src/HOL/Tools/BNF/bnf_tactics.ML
src/HOL/Tools/BNF/bnf_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/BNF/Tools/bnf_comp.ML
     1.5 +(*  Title:      HOL/Tools/BNF/bnf_comp.ML
     1.6      Author:     Dmitriy Traytel, TU Muenchen
     1.7      Author:     Jasmin Blanchette, TU Muenchen
     1.8      Copyright   2012
     2.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/BNF/Tools/bnf_comp_tactics.ML
     2.5 +(*  Title:      HOL/Tools/BNF/bnf_comp_tactics.ML
     2.6      Author:     Dmitriy Traytel, TU Muenchen
     2.7      Author:     Jasmin Blanchette, TU Muenchen
     2.8      Copyright   2012
     3.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Jan 20 18:24:56 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Jan 20 18:24:56 2014 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/BNF/Tools/bnf_def.ML
     3.5 +(*  Title:      HOL/Tools/BNF/bnf_def.ML
     3.6      Author:     Dmitriy Traytel, TU Muenchen
     3.7      Author:     Jasmin Blanchette, TU Muenchen
     3.8      Copyright   2012
     4.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/BNF/Tools/bnf_def_tactics.ML
     4.5 +(*  Title:      HOL/Tools/BNF/bnf_def_tactics.ML
     4.6      Author:     Dmitriy Traytel, TU Muenchen
     4.7      Author:     Jasmin Blanchette, TU Muenchen
     4.8      Copyright   2012
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_def_sugar.ML
     5.5 +(*  Title:      HOL/Tools/BNF/bnf_fp_def_sugar.ML
     5.6      Author:     Jasmin Blanchette, TU Muenchen
     5.7      Copyright   2012, 2013
     5.8  
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
     6.5 +(*  Title:      HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     6.6      Author:     Jasmin Blanchette, TU Muenchen
     6.7      Copyright   2012
     6.8  
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_n2m.ML
     7.5 +(*  Title:      HOL/Tools/BNF/bnf_fp_n2m.ML
     7.6      Author:     Dmitriy Traytel, TU Muenchen
     7.7      Copyright   2013
     7.8  
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
     8.5 +(*  Title:      HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
     8.6      Author:     Jasmin Blanchette, TU Muenchen
     8.7      Copyright   2013
     8.8  
     9.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     9.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_n2m_tactics.ML
     9.5 +(*  Title:      HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
     9.6      Author:     Dmitriy Traytel, TU Muenchen
     9.7      Copyright   2013
     9.8  
    10.1 --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Jan 20 18:24:56 2014 +0100
    10.2 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Jan 20 18:24:56 2014 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
    10.5 +(*  Title:      HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
    10.6      Author:     Lorenz Panny, TU Muenchen
    10.7      Author:     Jasmin Blanchette, TU Muenchen
    10.8      Copyright   2013
    11.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jan 20 18:24:56 2014 +0100
    11.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jan 20 18:24:56 2014 +0100
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_util.ML
    11.5 +(*  Title:      HOL/Tools/BNF/bnf_fp_util.ML
    11.6      Author:     Dmitriy Traytel, TU Muenchen
    11.7      Author:     Jasmin Blanchette, TU Muenchen
    11.8      Copyright   2012, 2013
    12.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
    12.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      HOL/BNF/Tools/bnf_gfp.ML
    12.5 +(*  Title:      HOL/Tools/BNF/bnf_gfp.ML
    12.6      Author:     Dmitriy Traytel, TU Muenchen
    12.7      Author:     Andrei Popescu, TU Muenchen
    12.8      Author:     Jasmin Blanchette, TU Muenchen
    13.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
    13.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
    13.5 +(*  Title:      HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
    13.6      Author:     Lorenz Panny, TU Muenchen
    13.7      Author:     Jasmin Blanchette, TU Muenchen
    13.8      Copyright   2013
    14.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    14.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
    14.5 +(*  Title:      HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
    14.6      Author:     Jasmin Blanchette, TU Muenchen
    14.7      Copyright   2013
    14.8  
    15.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    15.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      HOL/BNF/Tools/bnf_gfp_tactics.ML
    15.5 +(*  Title:      HOL/Tools/BNF/bnf_gfp_tactics.ML
    15.6      Author:     Dmitriy Traytel, TU Muenchen
    15.7      Author:     Andrei Popescu, TU Muenchen
    15.8      Author:     Jasmin Blanchette, TU Muenchen
    16.1 --- a/src/HOL/Tools/BNF/bnf_gfp_util.ML	Mon Jan 20 18:24:56 2014 +0100
    16.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML	Mon Jan 20 18:24:56 2014 +0100
    16.3 @@ -1,4 +1,4 @@
    16.4 -(*  Title:      HOL/BNF/Tools/bnf_gfp_util.ML
    16.5 +(*  Title:      HOL/Tools/BNF/bnf_gfp_util.ML
    16.6      Author:     Dmitriy Traytel, TU Muenchen
    16.7      Copyright   2012
    16.8  
    17.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jan 20 18:24:56 2014 +0100
    17.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jan 20 18:24:56 2014 +0100
    17.3 @@ -1,4 +1,4 @@
    17.4 -(*  Title:      HOL/BNF/Tools/bnf_lfp.ML
    17.5 +(*  Title:      HOL/Tools/BNF/bnf_lfp.ML
    17.6      Author:     Dmitriy Traytel, TU Muenchen
    17.7      Author:     Andrei Popescu, TU Muenchen
    17.8      Copyright   2012
    18.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jan 20 18:24:56 2014 +0100
    18.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jan 20 18:24:56 2014 +0100
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/BNF/Tools/bnf_lfp_compat.ML
    18.5 +(*  Title:      HOL/Tools/BNF/bnf_lfp_compat.ML
    18.6      Author:     Jasmin Blanchette, TU Muenchen
    18.7      Copyright   2013
    18.8  
    19.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
    19.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
    19.3 @@ -1,4 +1,4 @@
    19.4 -(*  Title:      HOL/BNF/Tools/bnf_lfp_rec_sugar.ML
    19.5 +(*  Title:      HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
    19.6      Author:     Lorenz Panny, TU Muenchen
    19.7      Author:     Jasmin Blanchette, TU Muenchen
    19.8      Copyright   2013
    20.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    20.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    20.3 @@ -1,4 +1,4 @@
    20.4 -(*  Title:      HOL/BNF/Tools/bnf_lfp_tactics.ML
    20.5 +(*  Title:      HOL/Tools/BNF/bnf_lfp_tactics.ML
    20.6      Author:     Dmitriy Traytel, TU Muenchen
    20.7      Author:     Andrei Popescu, TU Muenchen
    20.8      Copyright   2012
    21.1 --- a/src/HOL/Tools/BNF/bnf_lfp_util.ML	Mon Jan 20 18:24:56 2014 +0100
    21.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML	Mon Jan 20 18:24:56 2014 +0100
    21.3 @@ -1,4 +1,4 @@
    21.4 -(*  Title:      HOL/BNF/Tools/bnf_lfp_util.ML
    21.5 +(*  Title:      HOL/Tools/BNF/bnf_lfp_util.ML
    21.6      Author:     Dmitriy Traytel, TU Muenchen
    21.7      Author:     Jasmin Blanchette, TU Muenchen
    21.8      Copyright   2012
    22.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    22.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
    22.3 @@ -1,4 +1,4 @@
    22.4 -(*  Title:      HOL/BNF/Tools/bnf_tactics.ML
    22.5 +(*  Title:      HOL/Tools/BNF/bnf_tactics.ML
    22.6      Author:     Dmitriy Traytel, TU Muenchen
    22.7      Author:     Jasmin Blanchette, TU Muenchen
    22.8      Copyright   2012
    23.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Jan 20 18:24:56 2014 +0100
    23.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Jan 20 18:24:56 2014 +0100
    23.3 @@ -1,4 +1,4 @@
    23.4 -(*  Title:      HOL/BNF/Tools/bnf_util.ML
    23.5 +(*  Title:      HOL/Tools/BNF/bnf_util.ML
    23.6      Author:     Dmitriy Traytel, TU Muenchen
    23.7      Copyright   2012
    23.8