src/Tools/isac/ProgLang/ListC.thy
changeset 60586 007ef64dbb08
parent 60509 2e0b7ca391dc
child 60664 ed6f9e67349d
     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