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

Improved layout.

This commit is contained in:
Achim D. Brucker 2019-08-15 13:40:03 +01:00
parent 8eb233e6eb
commit 23f68ce6c8
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
examples/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -11,7 +11,7 @@ declare[[strict_monitor_checking=true]]
title*[title::title]\<open>The CENELEC 50128 Ontology\<close>
subtitle*[subtitle::subtitle]\<open>Case Study: An Odometer-Subsystem\<close>
chapter*[casestudy::technical]\<open>A Case-Study: An Odometer-Subsystem\<close>
chapter*[casestudy::technical]\<open>An Odometer-Subsystem\<close>
text\<open>
In our case study, we will follow the phases of analysis, design, and implementation of the
odometry function of a train. This software processes data from an odometer to compute the position,
@ -32,7 +32,7 @@ text\<open>
development.
\<close>
section\<open>System Requirements Specification as an \<^emph>\<open>Integrated Source\<close>\<close>
section\<open>System Requirements as an \<^emph>\<open>Integrated Source\<close>\<close>
text\<open>Accurate information of a train's location along a track is in an important prerequisite
to safe railway operation. Position, speed and acceleration measurement usually lies on a
set of independent measurements based on different physical principles---as a way to enhance
@ -46,9 +46,9 @@ text\<open>
related to the trains progress. By measuring the fractional rotation of the encoders shaft and
considering the wheels effective ratio, relative movement of the train can be calculated.
\begin{wrapfigure}[8]{l}{3.9cm}
\begin{wrapfigure}[8]{l}{4.6cm}
\centering
\vspace{-.7cm}
\vspace{-.5cm}
\includegraphics[width=3.4cm]{figures/wheel-df}
\caption{Motion sensing via an odometer.}
\label{wheel-df}