test/Tools/isac/Knowledge/algein.sml
changeset 59936 554030065b5b
parent 59912 dc53f7815edc
child 59983 f1fdb213717b
     1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Mon May 04 12:38:16 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Mon May 04 13:27:45 2020 +0200
     1.3 @@ -108,7 +108,6 @@
     1.4  val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
     1.5  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
     1.6  
     1.7 -(*testing code in ME/appl.sml*)
     1.8  val sube = ["?a1 = (3::real)"];
     1.9  val subte = Subst.input_to_terms sube;
    1.10  UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)