(* theory collecting all knowledge defined so far

    WN.11.00

  *)

 theory Isac 

 imports "~~/src/Tools/isac/Frontend/Frontend"

   PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*) 

   DiophantEq Inverse_Z_Transform Test

   (*THIS WAITS UNITL Isabelle2013 (? how include into dependency graph?).....

   ..... GCD_Poly_FP*)

 begin

 text {* dependencies alternative to those defined by R.Lang during his thesis:

    Poly				Root

      |\__________		 |

      |		 \ 		 |

      |		Rational	 |

      |		  |		 |

    PolyEq	RatEq		RootEq

       \         /  \           /

        \       /    \         /

 	RatPolyEq    RatRootEq    etc.

 *}

 ML {* val version_isac = "isac version 120504 15:33"; *}

 ML {* (* there are strange dependencies between tests:

          insert_fillpats in test/../thy_hierarchy.sml affects subsequent tests,

          see changeset 58e0a39e58b7.

          This function checks for data in ! mets, ! thehier set in Build_Thydata.thy *)

 fun check_unsynchronized_ref () =

   let

     val met = get_met ["diff","differentiate_on_R"];

     val {errpats, ...} = met;

     val hthm = get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"];

     val Hthm {fillpats, ...} = hthm;

     val hrls = get_the ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"];

     val Hrls {thy_rls = (thyID, rls), ...} = hrls

     val Rls {errpatts, ...} = rls;

   in

     case errpats of

       ("chain-rule-diff-both", _ :: _,_ :: _) :: _ => writeln "----- errpats original"

     | _ => writeln "##### errpats changed";

     case fillpats of

       ("fill-d_d-arg", _, "chain-rule-diff-both") :: ("fill-both-args", _, "chain-rule-diff-both") :: _ 

         => writeln "----- fillpats original"

     | _ => writeln "##### fillpats changed";

     case errpatts of 

       ["chain-rule-diff-both", "cancel"] => writeln "----- errpatIDs original"

     | _ => writeln "##### errpatIDs changed"

   end;

 *}

 end