diff --git a/examples/math_exam/On_Noodles.thy b/examples/math_exam/On_Noodles.thy new file mode 100644 index 0000000..967a9d8 --- /dev/null +++ b/examples/math_exam/On_Noodles.thy @@ -0,0 +1,32 @@ +theory "On_Noodles" + imports "../../ontologies/small_math" + "../../ontologies/technical_report" +begin + +open_monitor*[this::article] + +title*[t1::title]\On Noodles\ + +text*[simon::author]\Simon Foster\ +text*[a::abstract, keywordlist = "[topology]"] +\We present the first fundamental results on the goundbreaking theory of noodles...\ +section*[intro::introduction]\Introduction\ + +text\ Authorities say, that Noodles are unleavened dough which is stretched, + extruded, or rolled flat and cut into one or a variety of shapes which usually +include long, thin strips, or waves, helices, tubes, strings, or shells, or +folded over, or cut into other shapes. Noodles are usually cooked in boiling water, +sometimes with cooking oil or salt added. \ + +section*[def_sec::technical]\Basic definitions\ + +text*[d1::"definition"]\My first definition\ +definition noodle ::"bool" where "noodle = (THE x. True)" + +(* +update_instance*[def1, formal_results:="[@{thm ''noodle_def''}]"] +*) + +close_monitor*[this::article] + +end