1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sun Sep 22 17:28:55 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sun Sep 22 18:09:05 2013 +0200
1.3 @@ -248,8 +248,12 @@
1.4 ("diff_conv", prep_rls diff_conv),
1.5 ("diff_sym_conv", prep_rls diff_sym_conv)
1.6 ]);
1.7 -
1.8 *}
1.9 +setup {* KEStore_Elems.add_rlss
1.10 + [("diff_rules", (Context.theory_name @{theory}, prep_rls diff_rules)),
1.11 + ("norm_diff", (Context.theory_name @{theory}, prep_rls norm_diff)),
1.12 + ("diff_conv", (Context.theory_name @{theory}, prep_rls diff_conv)),
1.13 + ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls diff_sym_conv))] *}
1.14 ML {*
1.15 (** problem types **)
1.16