--- 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
--- 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
--- 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,
--- 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 =
--- 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 =
--- 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 =
--- 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 =
--- 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 =