test/Tools/isac/Test_Some.thy
changeset 60408 914e6413a66a
parent 60407 eca042e683b9
child 60409 432482c14d96
     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  (*