src/Tools/isac/ProgLang/Prog_Expr.thy
changeset 60312 35f7b2f61797
parent 60309 70a1d102660d
child 60313 8d89a214aedc
     1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 15:50:58 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 16:18:27 2021 +0200
     1.3 @@ -536,11 +536,11 @@
     1.4  
     1.5  rule_set_knowledge prog_expr = prog_expr
     1.6  setup \<open>KEStore_Elems.add_calcs
     1.7 -  [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
     1.8 -    ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),
     1.9 -    ("Vars", ("Prog_Expr.Vars", Prog_Expr.eval_var "#Vars_")),
    1.10 -    ("lhs", ("Prog_Expr.lhs", Prog_Expr.eval_lhs "")),
    1.11 -    ("rhs", ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""))]\<close>
    1.12 +  [("matches", (\<^const_name>\<open>matches\<close>, Prog_Expr.eval_matches "#matches_")),
    1.13 +    ("matchsub", (\<^const_name>\<open>matchsub\<close>, Prog_Expr.eval_matchsub "#matchsub_")),
    1.14 +    ("Vars", (\<^const_name>\<open>Vars\<close>, Prog_Expr.eval_var "#Vars_")),
    1.15 +    ("lhs", (\<^const_name>\<open>lhs\<close>, Prog_Expr.eval_lhs "")),
    1.16 +    ("rhs", (\<^const_name>\<open>rhs\<close>, Prog_Expr.eval_rhs ""))]\<close>
    1.17  (*\\------------------------- from Tools .thy-------------------------------------------------//*)
    1.18  ML \<open>
    1.19  \<close> ML \<open>