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