src/HOL/Transcendental.thy
changeset 68642 d812b6ee711b
parent 68638 87d1bff264df
child 68774 9fc50a3e07f6
     1.1 --- a/src/HOL/Transcendental.thy	Mon Jul 16 08:32:27 2018 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Jul 16 15:24:06 2018 +0200
     1.3 @@ -7199,6 +7199,7 @@
     1.4          SOME (Thm.instantiate' [] (map (SOME o Thm.cterm_of ctxt o HOLogic.mk_numeral) [m, n])
     1.5                    @{thm sqrt_numeral_simproc_aux})
     1.6    end
     1.7 +    handle TERM _ => NONE
     1.8  
     1.9  fun root_simproc (threshold1, threshold2) ctxt ct =
    1.10    let
    1.11 @@ -7212,6 +7213,8 @@
    1.12            SOME (Thm.instantiate' [] (map (SOME o Thm.cterm_of ctxt o HOLogic.mk_numeral) [m, n, x])
    1.13              @{thm root_numeral_simproc_aux})
    1.14    end
    1.15 +    handle TERM _ => NONE
    1.16 +         | Match => NONE
    1.17  
    1.18  fun powr_simproc (threshold1, threshold2) ctxt ct =
    1.19    let
    1.20 @@ -7233,6 +7236,8 @@
    1.21              SOME (@{thm transitive} OF [eq_thm, thm])
    1.22            end
    1.23    end
    1.24 +    handle TERM _ => NONE
    1.25 +         | Match => NONE
    1.26  
    1.27  end
    1.28  \<close>