Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

second pass. Small errors here and there. Version in interactive mode for testing - no session Isa_DOF yet.
HOL-OCL/Isabelle_DOF/Isabelle2018 This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-04-29 17:32:45 +02:00
parent f89471d422
commit 4a9e765cd3
1 changed files with 0 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
examples/math_exam/On_Noodle.thy
View File

@ -1,30 +0,0 @@
theory "On_Noodle"
imports small_math
begin
open_monitor*[this::article]
title*[t1::title]\<open>On Noodles\<close>
text*[simon::author]\<open>Simon Foster\<close>
text*[a::abstract, keyword_list = "[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]