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