src/HOL/HOL.thy
changeset 61222 05d28dc76e5c
parent 61202 9e37178084c5
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 21 21:43:09 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 21 21:46:14 2015 +0200
     1.3 @@ -1691,8 +1691,8 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 -text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
     1.8 -not to simplify the argument and to solve it by an assumption. *}
     1.9 +text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
    1.10 +not to simplify the argument and to solve it by an assumption.\<close>
    1.11  
    1.12  definition ASSUMPTION :: "bool \<Rightarrow> bool" where
    1.13  "ASSUMPTION A \<equiv> A"
    1.14 @@ -1706,7 +1706,7 @@
    1.15  lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
    1.16  by(simp add: ASSUMPTION_def)
    1.17  
    1.18 -setup {*
    1.19 +setup \<open>
    1.20  let
    1.21    val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
    1.22      resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
    1.23 @@ -1714,7 +1714,7 @@
    1.24  in
    1.25    map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
    1.26  end
    1.27 -*}
    1.28 +\<close>
    1.29  
    1.30  
    1.31  subsection \<open>Code generator setup\<close>