src/Tools/isac/ProgLang/ListC.thy
changeset 48761 4162c4f6f897
parent 42458 4d7502e18f18
child 48880 ea0c337066d9
     1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -6,14 +6,13 @@
     1.4  theory ListC imports Complex_Main
     1.5  uses ("../library.sml")
     1.6       ("../calcelems.sml")
     1.7 -     ("termC.sml")("calculate.sml")
     1.8 -     ("rewrite.sml")
     1.9 +     ("termC.sml") ("calculate.sml") ("rewrite.sml")
    1.10  begin
    1.11 -use "../library.sml"        (*indent,...*)
    1.12 -use "../calcelems.sml"      (*str_of_type, Thm,...*)
    1.13 -use "termC.sml"  (*num_str,...*)
    1.14 -use "calculate.sml" (*???*)
    1.15 -use "rewrite.sml"   (*?*** At command "end" (line 205../ListC.thy*)
    1.16 +use "../library.sml"
    1.17 +use "../calcelems.sml"
    1.18 +use "termC.sml"
    1.19 +use "calculate.sml"
    1.20 +use "rewrite.sml"
    1.21  
    1.22  text {* 'nat' in List.thy replaced by 'real' *}
    1.23