1.1 --- a/src/Tools/isac/ProgLang/ListC.thy Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -132,11 +132,11 @@
1.4 \<close> ML \<open>
1.5 val prog_expr =
1.6 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.7 - erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
1.8 + asm_rls = Rule_Def.Empty, prog_rls = Rule_Def.Empty, calc = [], errpatts = [],
1.9 rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
1.10 Rule_Def.Thm ("o_apply", @{thm o_apply}),
1.11
1.12 - Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
1.13 + Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*asm_rls for cond. in Atools.ML*)
1.14 Rule_Def.Thm ("NTH_NIL", @{thm NTH_NIL}),
1.15 Rule_Def.Thm ("append_Cons", @{thm append_Cons}),
1.16 Rule_Def.Thm ("append_Nil", @{thm append_Nil}),
1.17 @@ -176,7 +176,7 @@
1.18 Rule_Def.Thm ("tl_Nil", @{thm tl_Nil}),
1.19 Rule_Def.Thm ("zip_Cons", @{thm zip_Cons}),
1.20 Rule_Def.Thm ("zip_Nil", @{thm zip_Nil})],
1.21 - scr = Rule_Def.Empty_Prog}: Rule_Set.T;
1.22 + program = Rule_Def.Empty_Prog}: Rule_Set.T;
1.23 \<close>
1.24 rule_set_knowledge prog_expr = prog_expr
1.25