(* theory collecting all knowledge defined so far

   WN.11.00

 *)

theory Isac 

imports "../Frontend/Frontend"

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

  DiophantEq Inverse_Z_Transform Test

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