src/Tools/isac/ProgLang/ListC.thy
changeset 52135 9659f65c9df6
parent 52122 904bac7df4f6
child 52139 511fc271f783
     1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Sep 25 13:52:54 2013 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Sep 26 14:52:23 2013 +0200
     1.3 @@ -198,5 +198,10 @@
     1.4  setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
     1.5  
     1.6  ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF  Theory_Data*)*}
     1.7 -
     1.8 +ML {*
     1.9 +(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
    1.10 +  AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
    1.11 +  HERE IS ME_Isa: 'eval_rls' not in system ...*)
    1.12 +assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
    1.13 +*}
    1.14  end