1.1 --- a/test/Tools/isac/Test_Some.thy Fri Sep 24 14:18:10 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Sat Sep 25 13:54:06 2021 +0200
1.3 @@ -126,6 +126,9 @@
1.4 if UnparseC.term_in_ctxt @{context} t = "16"
1.5 then () else error "calcul 4 \<up> 2 \<longrightarrow> 16 corrected ? ";
1.6 \<close> ML \<open>
1.7 +val t = calcul @{theory} @{term "(- 1) \<up> 2"};
1.8 +if UnparseC.term_in_ctxt @{context} t = "(- 1) \<up> 2"
1.9 +then () else error "calcul (- 1) \<up> 2 \<longrightarrow> 1 corrected ? ";
1.10
1.11 (* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)
1.12 (*