
diff -r 9690a8d5f1c0 -r 904bac7df4f6 src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Thu Sep 19 15:51:03 2013 +0200
+++ b/src/Tools/isac/ProgLang/ListC.thy	Fri Sep 20 15:26:24 2013 +0200
@@ -1,20 +1,15 @@
-(* Title:  functions on lists for Scripts
+(* Title:  functions on lists for Programs
    Author: Walther Neuper 0108
    (c) due to copyright terms
 *)
 
-theory ListC imports Complex_Main
-uses ("~~/src/Tools/isac/library.sml")
-     ("~~/src/Tools/isac/calcelems.sml")
-     ("~~/src/Tools/isac/ProgLang/termC.sml") 
-     ("~~/src/Tools/isac/ProgLang/calculate.sml") 
-     ("~~/src/Tools/isac/ProgLang/rewrite.sml")
+theory ListC 
+imports Complex_Main "~~/src/Tools/isac/KEStore"
 begin
-use "~~/src/Tools/isac/library.sml"
-use "~~/src/Tools/isac/calcelems.sml"
-use "~~/src/Tools/isac/ProgLang/termC.sml"
-use "~~/src/Tools/isac/ProgLang/calculate.sml"
-use "~~/src/Tools/isac/ProgLang/rewrite.sml"
+
+ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
+ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
+ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
 
 text {* 'nat' in List.thy replaced by 'real' *}
 
@@ -200,4 +195,8 @@
   [("list_rls",list_rls)
    ]);
 *}
+setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
+
+ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF  Theory_Data*)*}
+
 end




