# HG changeset patch
# User wenzelm
# Date 1252765848 -7200
# Node ID 378528d2f7eb36dd9504b393e0fe61f3d0baf076
# Parent  c4a12569de89668e126c7a082453dc26a951a3d7
standard headers and text sections;

diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Mirabelle.thy
--- a/src/HOL/Mirabelle/Mirabelle.thy	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title: Mirabelle.thy
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Mirabelle.thy
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 theory Mirabelle
diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Mirabelle_Test.thy
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title: Mirabelle_Test.thy
-   Author: Sascha Boehme
+(*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
+    Author:     Sascha Boehme, TU Munich
 *)
 
 header {* Simple test theory for Mirabelle actions *}
@@ -14,9 +14,9 @@
   "Tools/mirabelle_sledgehammer.ML"
 begin
 
-(*
-  only perform type-checking of the actions,
-  any reasonable test would be too complicated
-*)
+text {*
+  Only perform type-checking of the actions,
+  any reasonable test would be too complicated.
+*}
 
 end
diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Sep 12 16:30:48 2009 +0200
@@ -1,17 +1,17 @@
-(* Title:  mirabelle.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 signature MIRABELLE =
 sig
-  (* configuration *)
+  (*configuration*)
   val logfile : string Config.T
   val timeout : int Config.T
   val start_line : int Config.T
   val end_line : int Config.T
   val setup : theory -> theory
 
-  (* core *)
+  (*core*)
   type init_action
   type done_action
   type run_action
@@ -21,7 +21,7 @@
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     unit
 
-  (* utility functions *)
+  (*utility functions*)
   val goal_thm_of : Proof.state -> thm
   val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
     Proof.state -> bool
@@ -47,10 +47,8 @@
 val setup = setup1 #> setup2 #> setup3 #> setup4
 
 
-
 (* Mirabelle core *)
 
-
 type init_action = int -> theory -> theory
 type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
 type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Tools/mirabelle_arith.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_arith.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_arith.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Arith : MIRABELLE_ACTION =
diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_metis.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_metis.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Metis : MIRABELLE_ACTION =
diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_quickcheck.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Tools/mirabelle_refute.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_refute.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_refute.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Refute : MIRABELLE_ACTION =
diff -r c4a12569de89 -r 378528d2f7eb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 11 09:53:02 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 12 16:30:48 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_sledgehammer.ML
-   Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
+    Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
 *)
 
 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =