1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -262,18 +262,18 @@
     1.4  (*evaluate identity
     1.5  > reflI;
     1.6  val it = "(?t = ?t) = True"
     1.7 -> val t = str2term "x = 0";
     1.8 +> val t = TermC.parse_test @{context} "x = 0";
     1.9  > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
    1.10  
    1.11 -> val t = str2term "1 = 0";
    1.12 +> val t = TermC.parse_test @{context} "1 = 0";
    1.13  > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
    1.14  ----------- thus needs Rule.Eval !
    1.15 -> val t = str2term "0 = 0";
    1.16 +> val t = TermC.parse_test @{context} "0 = 0";
    1.17  > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
    1.18  > UnparseC.term t';
    1.19  val it = \<^const_name>\<open>True\<close>
    1.20  
    1.21 -val t = str2term "Not (x = 0)";
    1.22 +val t = TermC.parse_test @{context} "Not (x = 0)";
    1.23  atomt t; UnparseC.term t;
    1.24  *** -------------
    1.25  *** Const ( Not)
    1.26 @@ -298,17 +298,17 @@
    1.27  	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.28    | eval_ident _ _ _ _ = NONE;
    1.29  (* TODO
    1.30 -> val t = str2term "x =!= 0";
    1.31 +> val t = TermC.parse_test @{context} "x =!= 0";
    1.32  > val SOME (str, t') = eval_ident "ident_" "b" t thy;
    1.33  > UnparseC.term t';
    1.34  val str = "ident_(x)_(0)" : string
    1.35  val it = "(x =!= 0) = False" : string                                
    1.36 -> val t = str2term "1 =!= 0";
    1.37 +> val t = TermC.parse_test @{context} "1 =!= 0";
    1.38  > val SOME (str, t') = eval_ident "ident_" "b" t thy;
    1.39  > UnparseC.term t';
    1.40  val str = "ident_(1)_(0)" : string 
    1.41  val it = "(1 =!= 0) = False" : string                                       
    1.42 -> val t = str2term "0 =!= 0";
    1.43 +> val t = TermC.parse_test @{context} "0 =!= 0";
    1.44  > val SOME (str, t') = eval_ident "ident_" "b" t thy;
    1.45  > UnparseC.term t';
    1.46  val str = "ident_(0)_(0)" : string