diff -r b7071d1dd263 -r 007ef64dbb08 src/Tools/isac/ProgLang/ListC.thy --- a/src/Tools/isac/ProgLang/ListC.thy Mon Oct 31 18:28:36 2022 +0100 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Nov 07 17:37:20 2022 +0100 @@ -132,11 +132,11 @@ \ ML \ val prog_expr = Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), - erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [], + asm_rls = Rule_Def.Empty, prog_rls = Rule_Def.Empty, calc = [], errpatts = [], rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) Rule_Def.Thm ("o_apply", @{thm o_apply}), - Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) + Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*asm_rls for cond. in Atools.ML*) Rule_Def.Thm ("NTH_NIL", @{thm NTH_NIL}), Rule_Def.Thm ("append_Cons", @{thm append_Cons}), Rule_Def.Thm ("append_Nil", @{thm append_Nil}), @@ -176,7 +176,7 @@ Rule_Def.Thm ("tl_Nil", @{thm tl_Nil}), Rule_Def.Thm ("zip_Cons", @{thm zip_Cons}), Rule_Def.Thm ("zip_Nil", @{thm zip_Nil})], - scr = Rule_Def.Empty_Prog}: Rule_Set.T; + program = Rule_Def.Empty_Prog}: Rule_Set.T; \ rule_set_knowledge prog_expr = prog_expr