1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Fri Sep 27 17:42:16 2013 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Sun Sep 29 18:27:37 2013 +0200
     1.3 @@ -141,10 +141,9 @@
     1.4  ML{* (*the former ListC.ML*)
     1.5  (** rule set for evaluating listexpr in scripts **)
     1.6  val list_rls = 
     1.7 -  Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
     1.8 -      erls = Erls, srls = Erls, calc = [], errpatts = [],
     1.9 -      rules = (*8.01: copied from*)
    1.10 -      [Thm ("refl", num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
    1.11 +  Rls{id = "list_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), 
    1.12 +    erls = Erls, srls = Erls, calc = [], errpatts = [],
    1.13 +    rules = [Thm ("refl", num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
    1.14         Thm ("o_apply", num_str @{thm o_apply}),
    1.15  
    1.16         Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
    1.17 @@ -186,22 +185,13 @@
    1.18         Thm ("tl_Cons",num_str @{thm tl_Cons}),
    1.19         Thm ("tl_Nil",num_str @{thm tl_Nil}),
    1.20         Thm ("zip_Cons",num_str @{thm zip_Cons}),
    1.21 -       Thm ("zip_Nil",num_str @{thm zip_Nil})
    1.22 -       ], scr = EmptyScr}:rls;
    1.23 +       Thm ("zip_Nil",num_str @{thm zip_Nil})],
    1.24 +    scr = EmptyScr}:rls;
    1.25  *}
    1.26  
    1.27  ML{*
    1.28 -ruleset' := overwritelthy @{theory} (!ruleset',
    1.29 -  [("list_rls",list_rls)
    1.30 -   ]);
    1.31 +ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
    1.32  *}
    1.33  setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
    1.34  
    1.35 -ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF  Theory_Data*)*}
    1.36 -ML {*
    1.37 -(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
    1.38 -  AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
    1.39 -  HERE IS ME_Isa: 'eval_rls' not in system ...*)
    1.40 -assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
    1.41 -*}
    1.42  end