tuning
authorblanchet
Tue Nov 19 18:38:25 2013 +0100 (2013-11-19 ago)
changeset 54504096f7d452164
parent 54503 b490e15a5e19
child 54505 d023838eb252
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Nov 19 18:34:04 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Tue Nov 19 18:38:25 2013 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  signature SLEDGEHAMMER_ANNOTATE =
     1.5  sig
     1.6    val annotate_types : Proof.context -> term -> term
     1.7 -end
     1.8 +end;
     1.9  
    1.10  structure Sledgehammer_Annotate : SLEDGEHAMMER_ANNOTATE =
    1.11  struct
    1.12 @@ -215,4 +215,4 @@
    1.13           |> sort int_ord
    1.14    in introduce_annotations subst typing_spots t t' end
    1.15  
    1.16 -end
    1.17 +end;
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Tue Nov 19 18:34:04 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Tue Nov 19 18:38:25 2013 +0100
     2.3 @@ -15,8 +15,7 @@
     2.4    type preplay_interface = Sledgehammer_Preplay.preplay_interface
     2.5  
     2.6    val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
     2.7 -end
     2.8 -
     2.9 +end;
    2.10  
    2.11  structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
    2.12  struct
    2.13 @@ -370,5 +369,4 @@
    2.14      do_proof proof
    2.15    end
    2.16  
    2.17 -
    2.18 -end
    2.19 +end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Tue Nov 19 18:34:04 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Tue Nov 19 18:38:25 2013 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4    type isar_proof = Sledgehammer_Proof.isar_proof
     3.5    val minimize_dependencies_and_remove_unrefed_steps :
     3.6      bool -> preplay_interface -> isar_proof -> isar_proof
     3.7 -end
     3.8 +end;
     3.9  
    3.10  structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
    3.11  struct
    3.12 @@ -105,4 +105,4 @@
    3.13      snd (do_proof proof)
    3.14    end
    3.15  
    3.16 -end
    3.17 +end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Tue Nov 19 18:34:04 2013 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Tue Nov 19 18:38:25 2013 +0100
     4.3 @@ -35,7 +35,7 @@
     4.4    val proof_preplay_interface :
     4.5      bool -> Proof.context -> string -> string -> bool -> Time.time
     4.6      -> isar_proof -> preplay_interface
     4.7 -end
     4.8 +end;
     4.9  
    4.10  structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
    4.11  struct
    4.12 @@ -312,4 +312,4 @@
    4.13          overall_preplay_stats = overall_preplay_stats}
    4.14      end
    4.15  
    4.16 -end
    4.17 +end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Tue Nov 19 18:34:04 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Tue Nov 19 18:38:25 2013 +0100
     5.3 @@ -293,4 +293,4 @@
     5.4              of_indent 0 ^ (if n <> 1 then "next" else "qed")
     5.5    end
     5.6  
     5.7 -end
     5.8 +end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Tue Nov 19 18:34:04 2013 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Tue Nov 19 18:38:25 2013 +0100
     6.3 @@ -67,7 +67,7 @@
     6.4  
     6.5    structure Canonical_Lbl_Tab : TABLE
     6.6  
     6.7 -end
     6.8 +end;
     6.9  
    6.10  structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
    6.11  struct
    6.12 @@ -196,4 +196,4 @@
    6.13      fst (do_proof proof (0, []))
    6.14    end
    6.15  
    6.16 -end
    6.17 +end;
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Tue Nov 19 18:34:04 2013 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Tue Nov 19 18:38:25 2013 +0100
     7.3 @@ -12,7 +12,7 @@
     7.4    type preplay_interface = Sledgehammer_Preplay.preplay_interface
     7.5  
     7.6    val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
     7.7 -end
     7.8 +end;
     7.9  
    7.10  structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
    7.11  struct
    7.12 @@ -59,4 +59,4 @@
    7.13  fun try0 preplay_timeout preplay_interface proof =
    7.14       map_isar_steps (try0_step preplay_timeout preplay_interface) proof
    7.15  
    7.16 -end
    7.17 +end;