1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Sat Sep 25 13:54:06 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Sat Sep 25 21:41:51 2021 +0200
     1.3 @@ -40,10 +40,16 @@
     1.4    by (simp_all add: inv_f_eq)
     1.5  
     1.6  lemma realpow_uminus_simps [simp]:
     1.7 +  "(- 1) \<up> 0 = 1"
     1.8 +  "(- 1) \<up> 1 = - 1"
     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 +  "odd (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (numeral n) = - 1"
    1.13 +  "even (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (- numeral n) = 1"
    1.14 +  "odd (numeral n :: nat) \<Longrightarrow> (- 1) \<up> (- numeral n) = - 1"
    1.15 +  "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = - (numeral m ^ numeral n)"
    1.16    "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = numeral m ^ numeral n"
    1.17 -  "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (numeral n) = - (numeral m ^ numeral n)"
    1.18    "even (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = 1 / (numeral m ^ numeral n)"
    1.19    "odd (numeral n :: nat) \<Longrightarrow> (- numeral m) \<up> (- numeral n) = - 1 / (numeral m ^ numeral n)"
    1.20    by (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq)

     2.1 --- a/test/Tools/isac/Test_Some.thy	Sat Sep 25 13:54:06 2021 +0200
     2.2 +++ b/test/Tools/isac/Test_Some.thy	Sat Sep 25 21:41:51 2021 +0200
     2.3 @@ -124,11 +124,11 @@
     2.4  *)
     2.5  val t = calcul @{theory} @{term "4 \<up> 2 ::real"};
     2.6  if UnparseC.term_in_ctxt @{context} t = "16"
     2.7 -then () else error "calcul  4 \<up> 2 \<longrightarrow> 16  corrected ? ";
     2.8 +then () else error "calcul  4 \<up> 2 \<longrightarrow> 16";
     2.9  \<close> ML \<open>
    2.10  val t = calcul @{theory} @{term "(- 1) \<up> 2"};
    2.11 -if UnparseC.term_in_ctxt @{context} t = "(- 1) \<up> 2" 
    2.12 -then () else error "calcul  (- 1) \<up> 2 \<longrightarrow> 1  corrected ? ";
    2.13 +if UnparseC.term_in_ctxt @{context} t = "1"
    2.14 +then () else error "calcul  (- 1) \<up> 2 \<longrightarrow> 1";
    2.15  
    2.16  (* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)
    2.17  (*