Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Rational.thy
changeset 60449 2406d378cede
parent 60405 d4ebe139100d
child 60500 59a3af532717 
     1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed Jun 01 13:39:41 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Jun 01 14:17:23 2022 +0200
     1.3 @@ -831,7 +831,7 @@
     1.4  
     1.5  problem pbl_simp_rat : "rational/simplification" =
     1.6    \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
     1.7 -  Method: "simplification/of_rationals"
     1.8 +  Method_Ref: "simplification/of_rationals"
     1.9    CAS: "Simplify t_t"
    1.10    Given: "Term t_t"
    1.11    Where: "t_t is_ratpolyexp"
wneuper/isa