1.1 --- a/src/Tools/isac/ProgLang/ListC.thy Thu Sep 19 15:51:03 2013 +0200
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Fri Sep 20 15:26:24 2013 +0200
1.3 @@ -1,20 +1,15 @@
1.4 -(* Title: functions on lists for Scripts
1.5 +(* Title: functions on lists for Programs
1.6 Author: Walther Neuper 0108
1.7 (c) due to copyright terms
1.8 *)
1.9
1.10 -theory ListC imports Complex_Main
1.11 -uses ("~~/src/Tools/isac/library.sml")
1.12 - ("~~/src/Tools/isac/calcelems.sml")
1.13 - ("~~/src/Tools/isac/ProgLang/termC.sml")
1.14 - ("~~/src/Tools/isac/ProgLang/calculate.sml")
1.15 - ("~~/src/Tools/isac/ProgLang/rewrite.sml")
1.16 +theory ListC
1.17 +imports Complex_Main "~~/src/Tools/isac/KEStore"
1.18 begin
1.19 -use "~~/src/Tools/isac/library.sml"
1.20 -use "~~/src/Tools/isac/calcelems.sml"
1.21 -use "~~/src/Tools/isac/ProgLang/termC.sml"
1.22 -use "~~/src/Tools/isac/ProgLang/calculate.sml"
1.23 -use "~~/src/Tools/isac/ProgLang/rewrite.sml"
1.24 +
1.25 +ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
1.26 +ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
1.27 +ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
1.28
1.29 text {* 'nat' in List.thy replaced by 'real' *}
1.30
1.31 @@ -200,4 +195,8 @@
1.32 [("list_rls",list_rls)
1.33 ]);
1.34 *}
1.35 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
1.36 +
1.37 +ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF Theory_Data*)*}
1.38 +
1.39 end