theory example_3 imports Isac

 begin

 section{*Function Decleration*}

 text{*Following code should only represent an example and was taken as a

       snipset from Rationals.thy located in 

       \texttt{/src/Tools/isac/Knowledge}*}

 (*----START----Example Function Decleration from Rationals.thy----*)

 text{*Define Method name and input, output types*}

 consts

   get_denominator :: "real => real"

 text{*Always add a comment with the method name and where it can be found.*}

 ML {*

 (*

  *("get_denominator",

  *  ("Rational.get_denominator", eval_get_denominator ""))

  *)

 fun eval_get_denominator (thmid:string) _ 

 		      (t as Const ("Rational.get_denominator", _) $

               (Const ("Rings.inverse_class.divide", _) $num 

                 $denom)) thy = 

         SOME (mk_thmid thmid "" 

             (Print_Mode.setmp [] 

               (Syntax.string_of_term (thy2ctxt thy)) denom) "", 

 	          Trueprop $ (mk_equality (t, denom)))

   | eval_get_denominator _ _ _ _ = NONE; 

 *}

 (*----END----Example Function Decleration from Rationals.thy----*)

 text{*Apply the Method to an expression.*}

 ML{*

   val input = term_of (the (parse thy "get_denominator ((a + b) / c)"));

   val SOME (_, output) = eval_get_denominator "" 0 input thy;

 *}

 ML{*

  term2str output;

 *}

 end