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

theory Test_Build_Thydata

imports "~~/src/Tools/isac/ProgLang/ProgLang"

begin

ML {*

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

*}

axiomatization where

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

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

ML {*

val rls111 = Rule.Rls {id = "rls111", 

	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule.e_rls, 

	srls = Rule.Erls, calc = [], errpatts = [],

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

	scr = Rule.EmptyScr};

val rls222 = Rule.Rls {id = "rls222", 

	preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule.e_rls, 

	srls = Rule.Erls, calc = [], errpatts = [],

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

	scr = Rule.EmptyScr};

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

*}

setup {* KEStore_Elems.add_rlss 

  [("rls111", (Context.theory_name @{theory}, prep_rls' rls111)),

   ("rls222", (Context.theory_name @{theory}, prep_rls' rls222))] *}

ML {*

  @{thm refl};

  @{thm o_def};

*}

end