src/Tools/isac/Knowledge/Simplify.thy
changeset 59279 255c853ea2f0
parent 59269 1da53d1540fe
child 59352 172b53399454
     1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4  (** CAS-command **)
     1.5  
     1.6  (*.function for handling the cas-input "Simplify (2*a + 3*a)":
     1.7 -   make a model which is already in ptree-internal format.*)
     1.8 +   make a model which is already in ctree-internal format.*)
     1.9  (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
    1.10     val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info.get_theory "Simplify"))) 
    1.11  				  "Simplify (2*a + 3*a)");