src/Tools/isac/ProgLang/Prog_Expr.thy
changeset 59801 17d807bf28fb
parent 59773 d88bb023c380
child 59841 aeeec4898fd1
     1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Feb 09 16:21:26 2020 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Feb 09 16:55:41 2020 +0100
     1.3 @@ -554,13 +554,13 @@
     1.4  
     1.5  subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
     1.6  ML \<open>
     1.7 -val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
     1.8 +val prog_expr = Rule.append_rls "prog_expr" prog_expr [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
     1.9  \<close> ML \<open>
    1.10  \<close> ML \<open>
    1.11  \<close>
    1.12  
    1.13  subsection \<open>setup for rule-sets and ML-functions\<close>
    1.14 -setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
    1.15 +setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
    1.16  setup \<open>KEStore_Elems.add_calcs
    1.17    [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
    1.18      ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),