9 imports |
9 imports |
10 (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) |
10 (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) |
11 (**)"$ISABELLE_ISAC/MathEngine/MathEngine" |
11 (**)"$ISABELLE_ISAC/MathEngine/MathEngine" |
12 (** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*) |
12 (** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*) |
13 keywords "Example" :: thy_decl |
13 keywords "Example" :: thy_decl |
14 and "Problem" "Specification" "Model" "References" "Solution" |
14 and "Specification" "Model" "References" "Solution" |
15 |
15 |
16 begin |
16 begin |
17 |
17 |
18 ML_file "parseC.sml" |
18 ML_file "parseC.sml" |
19 ML_file "preliminary.sml" |
19 ML_file "preliminary.sml" |
196 Ctree.EmptyPtree; |
196 Ctree.EmptyPtree; |
197 in set_data input thy end))); |
197 in set_data input thy end))); |
198 \<close> ML \<open> |
198 \<close> ML \<open> |
199 \<close> ML \<open> |
199 \<close> ML \<open> |
200 (*/----------------------------------------------------------------------------\*) |
200 (*/----------------------------------------------------------------------------\*) |
201 Parse.name -- Parse.!!! ( \<^keyword>\<open>Problem\<close> |-- Parse.name -- |
201 Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> -- |
202 Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> -- |
|
203 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input -- |
202 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_model_input -- |
204 Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input))) |
203 Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input)) |
205 : (string * (string * (Problem.model_input * references_input))) parser |
204 (*: (string * (Problem.model_input * references_input)) parser*) |
206 (*\----------------------------------------------------------------------------/*) |
205 (*\----------------------------------------------------------------------------/*) |
207 : Token.T list -> |
206 : Token.T list -> |
208 (*/----------------------------------------------------------------------------\*) |
207 (*/----------------------------------------------------------------------------\*) |
209 (string * (string * (Problem.model_input * references_input))) |
208 (string * (Problem.model_input * references_input)) |
210 (*\----------------------------------------------------------------------------/*) |
209 (*\----------------------------------------------------------------------------/*) |
211 * Token.T list |
210 * Token.T list |
212 (*/----------------------------------------------------------------------------\* ) |
211 (*/----------------------------------------------------------------------------\* ) |
213 the type above is the type of the argument of \<open>(fn (_(*name*),..\<close> |
212 the type above is the type of the argument of \<open>(fn (_(*name*),..\<close> |
214 ( *\----------------------------------------------------------------------------/*) |
213 ( *\----------------------------------------------------------------------------/*) |