standard headers and text sections;
authorwenzelm
Sat Sep 12 16:30:48 2009 +0200 (2009-09-12)
changeset 32564378528d2f7eb
parent 32563 c4a12569de89
child 32565 5047ab238cc0
standard headers and text sections;
src/HOL/Mirabelle/Mirabelle.thy
src/HOL/Mirabelle/Mirabelle_Test.thy
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Mirabelle/Tools/mirabelle_arith.ML
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
src/HOL/Mirabelle/Tools/mirabelle_refute.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
     1.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Fri Sep 11 09:53:02 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Sat Sep 12 16:30:48 2009 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4 -(* Title: Mirabelle.thy
     1.5 -   Author: Jasmin Blanchette and Sascha Boehme
     1.6 +(*  Title:      HOL/Mirabelle/Mirabelle.thy
     1.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     1.8  *)
     1.9  
    1.10  theory Mirabelle
     2.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Fri Sep 11 09:53:02 2009 +0200
     2.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sat Sep 12 16:30:48 2009 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4 -(* Title: Mirabelle_Test.thy
     2.5 -   Author: Sascha Boehme
     2.6 +(*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
     2.7 +    Author:     Sascha Boehme, TU Munich
     2.8  *)
     2.9  
    2.10  header {* Simple test theory for Mirabelle actions *}
    2.11 @@ -14,9 +14,9 @@
    2.12    "Tools/mirabelle_sledgehammer.ML"
    2.13  begin
    2.14  
    2.15 -(*
    2.16 -  only perform type-checking of the actions,
    2.17 -  any reasonable test would be too complicated
    2.18 -*)
    2.19 +text {*
    2.20 +  Only perform type-checking of the actions,
    2.21 +  any reasonable test would be too complicated.
    2.22 +*}
    2.23  
    2.24  end
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Sep 11 09:53:02 2009 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Sep 12 16:30:48 2009 +0200
     3.3 @@ -1,17 +1,17 @@
     3.4 -(* Title:  mirabelle.ML
     3.5 -   Author: Jasmin Blanchette and Sascha Boehme
     3.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle.ML
     3.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     3.8  *)
     3.9  
    3.10  signature MIRABELLE =
    3.11  sig
    3.12 -  (* configuration *)
    3.13 +  (*configuration*)
    3.14    val logfile : string Config.T
    3.15    val timeout : int Config.T
    3.16    val start_line : int Config.T
    3.17    val end_line : int Config.T
    3.18    val setup : theory -> theory
    3.19  
    3.20 -  (* core *)
    3.21 +  (*core*)
    3.22    type init_action
    3.23    type done_action
    3.24    type run_action
    3.25 @@ -21,7 +21,7 @@
    3.26    val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
    3.27      unit
    3.28  
    3.29 -  (* utility functions *)
    3.30 +  (*utility functions*)
    3.31    val goal_thm_of : Proof.state -> thm
    3.32    val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
    3.33      Proof.state -> bool
    3.34 @@ -47,10 +47,8 @@
    3.35  val setup = setup1 #> setup2 #> setup3 #> setup4
    3.36  
    3.37  
    3.38 -
    3.39  (* Mirabelle core *)
    3.40  
    3.41 -
    3.42  type init_action = int -> theory -> theory
    3.43  type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
    3.44  type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 11 09:53:02 2009 +0200
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Sep 12 16:30:48 2009 +0200
     4.3 @@ -1,5 +1,5 @@
     4.4 -(* Title:  mirabelle_arith.ML
     4.5 -   Author: Jasmin Blanchette and Sascha Boehme
     4.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_arith.ML
     4.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     4.8  *)
     4.9  
    4.10  structure Mirabelle_Arith : MIRABELLE_ACTION =
     5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 11 09:53:02 2009 +0200
     5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat Sep 12 16:30:48 2009 +0200
     5.3 @@ -1,5 +1,5 @@
     5.4 -(* Title:  mirabelle_metis.ML
     5.5 -   Author: Jasmin Blanchette and Sascha Boehme
     5.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_metis.ML
     5.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     5.8  *)
     5.9  
    5.10  structure Mirabelle_Metis : MIRABELLE_ACTION =
     6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 11 09:53:02 2009 +0200
     6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Sep 12 16:30:48 2009 +0200
     6.3 @@ -1,5 +1,5 @@
     6.4 -(* Title:  mirabelle_quickcheck.ML
     6.5 -   Author: Jasmin Blanchette and Sascha Boehme
     6.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
     6.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     6.8  *)
     6.9  
    6.10  structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
     7.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Sep 11 09:53:02 2009 +0200
     7.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Sat Sep 12 16:30:48 2009 +0200
     7.3 @@ -1,5 +1,5 @@
     7.4 -(* Title:  mirabelle_refute.ML
     7.5 -   Author: Jasmin Blanchette and Sascha Boehme
     7.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_refute.ML
     7.7 +    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     7.8  *)
     7.9  
    7.10  structure Mirabelle_Refute : MIRABELLE_ACTION =
     8.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 11 09:53:02 2009 +0200
     8.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 12 16:30:48 2009 +0200
     8.3 @@ -1,5 +1,5 @@
     8.4 -(* Title:  mirabelle_sledgehammer.ML
     8.5 -   Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow
     8.6 +(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
     8.7 +    Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
     8.8  *)
     8.9  
    8.10  structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =