src/HOL/Mirabelle/Mirabelle_Test.thy
changeset 32564 378528d2f7eb
parent 32518 e3c4e337196c
child 38892 eccc9e2a6412
     1.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Fri Sep 11 09:53:02 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sat Sep 12 16:30:48 2009 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4 -(* Title: Mirabelle_Test.thy
     1.5 -   Author: Sascha Boehme
     1.6 +(*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
     1.7 +    Author:     Sascha Boehme, TU Munich
     1.8  *)
     1.9  
    1.10  header {* Simple test theory for Mirabelle actions *}
    1.11 @@ -14,9 +14,9 @@
    1.12    "Tools/mirabelle_sledgehammer.ML"
    1.13  begin
    1.14  
    1.15 -(*
    1.16 -  only perform type-checking of the actions,
    1.17 -  any reasonable test would be too complicated
    1.18 -*)
    1.19 +text {*
    1.20 +  Only perform type-checking of the actions,
    1.21 +  any reasonable test would be too complicated.
    1.22 +*}
    1.23  
    1.24  end