src/HOL/Boogie/Tools/boogie_tactics.ML
changeset 47432 e1576d13e933
parent 46464 4cf5a84e2c05
     1.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -45,12 +45,12 @@
     1.4      in tac ctxt (thms @ facts) end))
     1.5  
     1.6  val setup_boogie = Method.setup @{binding boogie} (boogie_method false)
     1.7 -  ("Applies an SMT solver to the current goal " ^
     1.8 -   "using the current set of Boogie background axioms")
     1.9 +  "apply an SMT solver to the current goal \
    1.10 +  \using the current set of Boogie background axioms"
    1.11  
    1.12  val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true)
    1.13 -  ("Applies an SMT solver to all goals " ^
    1.14 -   "using the current set of Boogie background axioms")
    1.15 +  "apply an SMT solver to all goals \
    1.16 +  \using the current set of Boogie background axioms"
    1.17  
    1.18  
    1.19  local
    1.20 @@ -96,7 +96,7 @@
    1.21  in
    1.22  val setup_boogie_cases = Method.setup @{binding boogie_cases}
    1.23    (Scan.succeed boogie_cases)
    1.24 -  "Prepares a set of Boogie assertions for case-based proofs"
    1.25 +  "prepare a set of Boogie assertions for case-based proofs"
    1.26  end
    1.27  
    1.28