test/Tools/isac/Test_Some.thy
changeset 60407 eca042e683b9
parent 60406 66aeb9b614ab
child 60408 914e6413a66a
     1.1 --- a/test/Tools/isac/Test_Some.thy	Thu Sep 23 13:47:16 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Fri Sep 24 14:18:10 2021 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4    if-then-else \<and> < \<ge> even_real odd_real are possible reasons for insufficiency.
     1.5  *)
     1.6  val t = calcul @{theory} @{term "4 \<up> 2 ::real"};
     1.7 -if UnparseC.term_in_ctxt @{context} t = "4 \<up> 2"
     1.8 +if UnparseC.term_in_ctxt @{context} t = "16"
     1.9  then () else error "calcul  4 \<up> 2 \<longrightarrow> 16  corrected ? ";
    1.10  \<close> ML \<open>
    1.11