1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Sun Sep 26 20:58:57 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Mon Sep 27 13:14:09 2021 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  lemma realpow_uminus_simps [simp]:
     1.5    "(- 1) \<up> 0 = 1"
     1.6    "(- 1) \<up> 1 = - 1"
     1.7 -(** )"a \<up> (- 1) = 1 / a"( **)
     1.8 +  "z \<up> (- 1) = 1 / z"
     1.9    "(- numeral m) \<up> 0 = 1"
    1.10    "(- numeral m) \<up> 1 = - numeral m"
    1.11    "even (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (numeral n) = 1"
    1.12 @@ -53,12 +53,12 @@
    1.13    "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = numeral m ^ numeral n"
    1.14    "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = 1 / (numeral m ^ numeral n)"
    1.15    "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = - 1 / (numeral m ^ numeral n)"
    1.16 -(**)sledgehammer(**)
    1.17 -(**)by (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq)(**)
    1.18 +  apply (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq)
    1.19 +  by (simp add: powr_minus_divide)
    1.20  
    1.21    ML_file termC.sml
    1.22    ML_file substitution.sml
    1.23 -ML_file contextC.sml
    1.24 +  ML_file contextC.sml
    1.25    ML_file environment.sml
    1.26  
    1.27  ML \<open>

     2.1 --- a/src/Tools/isac/ProgLang/Calculate.thy	Sun Sep 26 20:58:57 2021 +0200
     2.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy	Mon Sep 27 13:14:09 2021 +0200
     2.3 @@ -67,11 +67,8 @@
     2.4  
     2.5  \<close> ML \<open>
     2.6  val t = calcul @{theory}      @{term "3 \<up> - 1"};
     2.7 -UnparseC.term_in_ctxt @{context} t = "3 \<up> - 1" (* ERROR: Simplifier.rewrite INEFFECTIVE *)
     2.8 -(*
     2.9  if UnparseC.term_in_ctxt @{context} t = "1 / 3"
    2.10  then () else error  "calcul  3 \<up> - 1 \<longrightarrow> 1 / 3";
    2.11 -*)
    2.12  \<close> ML \<open>
    2.13  
    2.14  (* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)