src/Tools/isac/Knowledge/Diff.thy
changeset 52125 6f1d3415dc68
parent 42458 4d7502e18f18
child 52142 e7febad0c988
     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