1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Sat Mar 17 13:43:24 2012 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Mar 19 09:48:03 2012 +0100
     1.3 @@ -5,6 +5,16 @@
     1.4  
     1.5  theory Equation imports Atools begin
     1.6  
     1.7 +text {* univariate equations over terms :
     1.8 +  In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing
     1.9 +  the Lucas-Interpreter's Subproblem mechanism.
    1.10 +  This prototype suffers from the drop-out of Matthias Goldgruber for a year,
    1.11 +  who had started to work on simplification in parallel. So this implementation
    1.12 +  replaced simplifiers by many specific theorems for specific terms in specific
    1.13 +  phases of equation solving; these specific solutions wait for generalisation
    1.14 +  in future improvements of ISAC's equation solver.
    1.15 +*}
    1.16 +
    1.17  consts
    1.18  
    1.19    (*descriptions in the related problems TODOshift here from Descriptions.thy*)