neuper@37906: (* simplification of terms
neuper@37906:    author: Walther Neuper 050912
neuper@37906:    (c) due to copyright terms
neuper@37906: 
neuper@37906: remove_thy"Simplify";
neuper@37906: use_thy"~/proto2/isac/src/sml/IsacKnowledge/Simplify";
neuper@37906: 
neuper@37906: use_thy_only"~/proto2/isac/src/sml/IsacKnowledge/Simplify";
neuper@37906: use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";
neuper@37906: *)
neuper@37906: 
neuper@37906: Simplify = Atools +
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   (*descriptions in the related problem*)
neuper@37906:   term        :: real => una
neuper@37906:   normalform  :: real => una
neuper@37906: 
neuper@37906:   (*the CAS-command*)
neuper@37906:   Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)
neuper@37906:   Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)
neuper@37906: 
neuper@37906:   (*Script-name*)
neuper@37906:   SimplifyScript      :: "[real,  real] => real"
neuper@37906:                   ("((Script SimplifyScript (_ =))// (_))" 9)
neuper@37906: 
neuper@37906: 
neuper@37906: end