src/Tools/isac/Knowledge/Rational.thy
changeset 60313 8d89a214aedc
parent 60312 35f7b2f61797
child 60331 40eb8aa2b0d6
     1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jun 21 16:18:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jun 21 20:06:12 2021 +0200
     1.3 @@ -458,8 +458,7 @@
     1.4  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
     1.5    | eval_is_expanded _ _ _ _ = NONE;
     1.6  \<close>
     1.7 -setup \<open>KEStore_Elems.add_calcs
     1.8 -  [("is_expanded", (\<^const_name>\<open>is_expanded\<close>, eval_is_expanded ""))]\<close>
     1.9 +calculation is_expanded = \<open>eval_is_expanded ""\<close>
    1.10  ML \<open>
    1.11  val rational_erls = 
    1.12    Rule_Set.merge "rational_erls" calculate_Rational