1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Sat Jun 12 18:22:07 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Sat Jun 12 18:27:30 2021 +0200
     1.3 @@ -50,22 +50,22 @@
     1.4    Rule_Def.Repeat {
     1.5      id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = Rule_Set.empty,
     1.6      srls = Rule_Set.empty, calc = [], rules = [
     1.7 -      Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
     1.8 -	    Rule.Thm ("xfoldr_Cons", @{thm xfoldr_Cons} (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *)),
     1.9 +      \<^rule_thm>\<open>xfoldr_Nil\<close> (*num_str*) (* foldr ?f [] = id *),
    1.10 +	    \<^rule_thm>\<open>xfoldr_Cons\<close> (* foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs *),
    1.11  
    1.12 -	    Rule.Thm ("ins_Nil", @{thm ins_Nil} (* ins ?i [] = [?i] *)),
    1.13 -	    Rule.Thm ("ins_Cons", @{thm ins_Cons} (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *)),
    1.14 -	    Rule.Thm ("sort_deff", @{thm sort_deff} (* InsSort.sort ?xs = foldr ins ?xs [] *)),
    1.15 +	    \<^rule_thm>\<open>ins_Nil\<close> (* ins ?i [] = [?i] *),
    1.16 +	    \<^rule_thm>\<open>ins_Cons\<close> (* ins ?i (?x # ?xs) = (if ?i < ?x then ?i # ?x # ?xs else ?x # ins ?i ?xs) *),
    1.17 +	    \<^rule_thm>\<open>sort_deff\<close> (* InsSort.sort ?xs = foldr ins ?xs [] *),
    1.18  
    1.19 -	    Rule.Thm ("o_id", @{thm o_id} (* ?f \<circ> id = ?f *)),
    1.20 -	    Rule.Thm ("o_assoc", @{thm o_assoc} (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *)),
    1.21 -	    Rule.Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
    1.22 -	    Rule.Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
    1.23 -      
    1.24 +	    \<^rule_thm>\<open>o_id\<close> (* ?f \<circ> id = ?f *),
    1.25 +	    \<^rule_thm>\<open>o_assoc\<close> (* ?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h *),
    1.26 +	    \<^rule_thm>\<open>o_apply\<close> (* (?f \<circ> ?g) ?x = ?f (?g ?x) *),
    1.27 +	    \<^rule_thm>\<open>id_apply\<close> (* id ?x = ?x *),
    1.28 +
    1.29  	    \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.30 -	    Rule.Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),
    1.31 -	    Rule.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
    1.32 -	    Rule.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
    1.33 +	    \<^rule_thm>\<open>If_def\<close> (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *),
    1.34 +	    \<^rule_thm>\<open>if_True\<close> (* "(if True then x else y) = x" *),
    1.35 +	    \<^rule_thm>\<open>if_False\<close> (* "(if False then x else y) = y" *)],
    1.36  	  errpatts = [], scr = Rule.Empty_Prog};      
    1.37  \<close>
    1.38  rule_set_knowledge ins_sort = ins_sort