First Port of Isa_DOF to Isabelle2018 (without LaTeX Generation; Front-End Unit-Tested)
HOL-OCL/Isabelle_DOF/Isabelle2018 This commit looks good
Details
HOL-OCL/Isabelle_DOF/Isabelle2018 This commit looks good
Details
This commit is contained in:
parent
b035996d36
commit
f89471d422
|
@ -0,0 +1,32 @@
|
||||||
|
theory "On_Noodles"
|
||||||
|
imports "../../ontologies/small_math"
|
||||||
|
"../../ontologies/technical_report"
|
||||||
|
begin
|
||||||
|
|
||||||
|
open_monitor*[this::article]
|
||||||
|
|
||||||
|
title*[t1::title]\<open>On Noodles\<close>
|
||||||
|
|
||||||
|
text*[simon::author]\<open>Simon Foster\<close>
|
||||||
|
text*[a::abstract, keywordlist = "[topology]"]
|
||||||
|
\<open>We present the first fundamental results on the goundbreaking theory of noodles...\<close>
|
||||||
|
section*[intro::introduction]\<open>Introduction\<close>
|
||||||
|
|
||||||
|
text\<open> 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. \<close>
|
||||||
|
|
||||||
|
section*[def_sec::technical]\<open>Basic definitions\<close>
|
||||||
|
|
||||||
|
text*[d1::"definition"]\<open>My first definition\<close>
|
||||||
|
definition noodle ::"bool" where "noodle = (THE x. True)"
|
||||||
|
|
||||||
|
(*
|
||||||
|
update_instance*[def1, formal_results:="[@{thm ''noodle_def''}]"]
|
||||||
|
*)
|
||||||
|
|
||||||
|
close_monitor*[this::article]
|
||||||
|
|
||||||
|
end
|
Loading…
Reference in New Issue