(* Minimal Thydata for test/../thy-hierarchy *)

 theory Test_Build_Thydata

   imports "Specify.ProgLang"

 begin

 ML \<open>

 open Rule

 fun termlessI (_: subst) uv = LibraryC.termless uv;

 \<close>

 axiomatization where

   thm111: "thm111 = thm111 + (111::int)" and

   thm222: "thm222 = thm222 + (222::int)"

 ML \<open>

 val rls111 = Rule_Def.Repeat {id = "rls111", 

 	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule_Set.empty, 

 	srls = Rule_Set.Empty, calc = [], errpatts = [],

 	rules = [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})],

 	scr = Rule.Empty_Prog};

 val rls222 = Rule_Def.Repeat {id = "rls222", 

 	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule_Set.empty, 

 	srls = Rule_Set.Empty, calc = [], errpatts = [],

 	rules = [Rule.Thm ("sym_thm111", @{thm thm111} RS @{thm sym}), Rule.Thm ("o_def", @{thm o_def})],

 	scr = Rule.Empty_Prog};

 val prep_rls' = Auto_Prog.prep_rls @{theory};

 \<close>

 setup_rule

   rls111 = \<open>prep_rls' rls111\<close> and

   rls222 = \<open>prep_rls' rls222\<close>

 ML \<open>

   @{thm refl};

   @{thm o_def};

 \<close> ML \<open>

 val [aaa, bbb, ccc, ddd, eee] = KEStore_Elems.get_rlss @{theory};

 \<close> ML \<open>

 if eq_set op = (map fst [aaa, bbb, ccc], ["e_rrls", "empty", "prog_expr"]) then ()

 else raise ERROR "test/../thy-hierarchy CHANGED"

 \<close> ML \<open>

 case ddd of

   ("rls111",

     ("Test_Build_Thydata",

      Rule_Def.Repeat {calc = [], erls =

           Rule_Def.Repeat {calc = [], erls = Rule_Set.Empty, errpatts = [], id = "empty", preconds = [], rew_ord =

                ("dummy_ord", _), rules = [], scr = Empty_Prog, srls = Rule_Set.Empty},

           errpatts = [], id = "rls111", preconds = [], rew_ord = ("termlessI", _), rules =

           [Thm ("thm111", _), Thm ("refl", _)], scr = Empty_Prog, srls = Rule_Set.Empty})) => ()

 | _ => raise ERROR "test/../thy-hierarchy CHANGED 4";

 \<close> ML \<open>

 case eee of

   ("rls222",

     ("Test_Build_Thydata",

      Rule_Def.Repeat {calc = [], erls =

           Rule_Def.Repeat {calc = [], erls = Rule_Set.Empty, errpatts = [], id = "empty", preconds = [], rew_ord =

                ("dummy_ord", _), rules = [], scr = Empty_Prog, srls = Rule_Set.Empty},

           errpatts = [], id = "rls222", preconds = [], rew_ord = ("termlessI", _), rules =

           [Thm ("sym_thm111", _), Thm ("o_def", _)], scr = Empty_Prog, srls = Rule_Set.Empty})) => ()

 | _ => raise ERROR "test/../thy-hierarchy CHANGED 5";

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close>

 end