1.1 --- a/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sat Sep 08 23:11:53 2012 +0200
     1.2 +++ b/doc-src/isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Sep 09 10:57:54 2012 +0200
     1.3 @@ -853,33 +853,46 @@
     1.4  
     1.5  \subsubsection{Find a place to Store the Function}
     1.6  The whole system builds up on a well defined structure of Knowledge. This
     1.7 -Knowledge sets up at\ttfamily src/Tools/isac/Knowledge\normalfont. For the
     1.8 -implementation of the Function \texttt{get\_denominator}, which let us now
     1.9 -the denominator of a fraction we have choosen the Theory (file)
    1.10 +Knowledge sets up at the Path: \ttfamily src/Tools/isac/Knowledge\normalfont.
    1.11 +For implementing the Function \texttt{get\_denominator} (which let us extract
    1.12 +the denominator out of a fraction) we have choosen the Theory (file)
    1.13  \texttt{Rational.thy}.
    1.14  
    1.15  \subsubsection{Write down the new Function}
    1.16 +In upper Theory we now define the new function and its purpose:
    1.17 +\begin{verbatim}
    1.18 +  get_denominator :: "real => real"
    1.19 +\end{verbatim}
    1.20 +This command tells the machine that a function with the name
    1.21 +\texttt{get\_denominator} exists which gets a real expression as argument and
    1.22 +returns once again a real expression. Now we are able to implement the function itself, Example~\ref{eg:getdenom}
    1.23 +shows the implementation of \texttt{get\_denominator}.
    1.24  
    1.25  \begin{example}
    1.26 -\begin{verbatim}
    1.27 +  \label{eg:getdenom}
    1.28 +  \begin{verbatim}
    1.29  
    1.30 -ML {*
    1.31 -(*
    1.32 - *("get_denominator",
    1.33 - *  ("Rational.get_denominator", eval_get_denominator ""))
    1.34 - *)
    1.35 -fun eval_get_denominator (thmid:string) _ 
    1.36 -          (t as Const ("Rational.get_denominator", _) $
    1.37 -              (Const ("Rings.inverse_class.divide", _) $num 
    1.38 -                $denom)) thy = 
    1.39 -        SOME (mk_thmid thmid "" 
    1.40 -            (Print_Mode.setmp [] 
    1.41 -              (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
    1.42 -            Trueprop $ (mk_equality (t, denom)))
    1.43 -  | eval_get_denominator _ _ _ _ = NONE; 
    1.44 -*}\end{verbatim}
    1.45 +01  (*
    1.46 +02   *("get_denominator",
    1.47 +03   *  ("Rational.get_denominator", eval_get_denominator ""))
    1.48 +04   *)
    1.49 +05  fun eval_get_denominator (thmid:string) _ 
    1.50 +06            (t as Const ("Rational.get_denominator", _) $
    1.51 +07                (Const ("Rings.inverse_class.divide", _) $num 
    1.52 +08                  $denom)) thy = 
    1.53 +09          SOME (mk_thmid thmid "" 
    1.54 +10              (Print_Mode.setmp [] 
    1.55 +11                (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
    1.56 +12              Trueprop $ (mk_equality (t, denom)))
    1.57 +13    | eval_get_denominator _ _ _ _ = NONE;\end{verbatim}
    1.58  \end{example}
    1.59  
    1.60 +Line \texttt{07} and \texttt{08} are describing the mode of operation the best -
    1.61 +there is a fraction\\ (\ttfamily Rings.inverse\_class.divide\normalfont) 
    1.62 +splittet
    1.63 +into its two parts (\texttt{ \$num \$denom}). The lines before are additionals
    1.64 +commands for declaring the function and the lines after are modeling and 
    1.65 +returning a real variable out of \texttt{\$denom}.
    1.66  
    1.67  \subsubsection{Add a test for the new Function}
    1.68  \subsubsection{Use the new Function}