equal
deleted
inserted
replaced
11 Errors are rigorously detected by isabelle build. |
11 Errors are rigorously detected by isabelle build. |
12 *) |
12 *) |
13 |
13 |
14 theory Build_Isac |
14 theory Build_Isac |
15 imports |
15 imports |
16 (* theory KEStore imports Complex_Main |
16 (* theory Know_Store imports Complex_Main |
17 ML_file libraryC.sml |
17 ML_file libraryC.sml |
18 ML_file theoryC.sml |
18 ML_file theoryC.sml |
19 ML_file unparseC.sml |
19 ML_file unparseC.sml |
20 ML_file "rule-def.sml" |
20 ML_file "rule-def.sml" |
21 ML_file thmC.sml |
21 ML_file thmC.sml |
23 ML_file "rewrite-order.sml" |
23 ML_file "rewrite-order.sml" |
24 ML_file rule.sml |
24 ML_file rule.sml |
25 ML_file "error-fill-def.sml" |
25 ML_file "error-fill-def.sml" |
26 ML_file "rule-set.sml" |
26 ML_file "rule-set.sml" |
27 ML_file calcelems.sml |
27 ML_file calcelems.sml |
28 theory BaseDefinitions imports KEStore |
28 theory BaseDefinitions imports Know_Store |
29 ML_file termC.sml |
29 ML_file termC.sml |
30 ML_file contextC.sml |
30 ML_file contextC.sml |
31 ML_file environment.sml |
31 ML_file environment.sml |
32 *) "BaseDefinitions/BaseDefinitions" |
32 *) "BaseDefinitions/BaseDefinitions" |
33 |
33 |
145 Mathias Lehnfeld gives the following list in his thesis in section |
145 Mathias Lehnfeld gives the following list in his thesis in section |
146 4.2.3 Relation to Ongoing Isabelle Development. |
146 4.2.3 Relation to Ongoing Isabelle Development. |
147 \<close> |
147 \<close> |
148 subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close> |
148 subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close> |
149 text \<open> |
149 text \<open> |
150 REPLACE BY KEStore... (has been overlooked) |
150 REPLACE BY Know_Store... (has been overlooked) |
151 calcelems.sml:val rew_ord' = Unsynchronized.ref ... |
151 calcelems.sml:val rew_ord' = Unsynchronized.ref ... |
152 KEEP FOR TRACING |
152 KEEP FOR TRACING |
153 calcelems.sml:val trace_rewrite = Unsynchronized.ref false; |
153 calcelems.sml:val trace_rewrite = Unsynchronized.ref false; |
154 calcelems.sml:val depth = Unsynchronized.ref 99999; |
154 calcelems.sml:val depth = Unsynchronized.ref 99999; |
155 calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999; |
155 calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999; |