src/Tools/isac/calcelems.sml
branchisac-update-Isa09-2
changeset 38011 3147f2c1525c
parent 38007 d679c1f837a7
child 38013 e4f42a63d665
     1.1 --- a/src/Tools/isac/calcelems.sml	Tue Sep 14 15:46:56 2010 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Sep 23 08:43:36 2010 +0200
     1.3 @@ -283,17 +283,17 @@
     1.4      (see match_ags).
     1.5  
     1.6      Preliminary solution:
     1.7 -    # the thy in 'SubProblem (thy_, pbl, arglist)' is not taken automatically,
     1.8 -    # instead the 'maxthy (rootthy pt) thy_' is taken for each subpbl
     1.9 +    # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
    1.10 +    # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
    1.11      # however, a thy specified by the user in the rootpbl may lead to 
    1.12        errors in far-off subpbls (which are not yet reported properly !!!) 
    1.13        and interactively specifiying thys in subpbl is not very relevant.
    1.14  
    1.15      Other solutions possible:
    1.16 -    # always parse and type-check with Isac.thy
    1.17 +    # always parse and type-check with theory "Isac"
    1.18        (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
    1.19      # regard the subthy-relation in specifying thys of subpbls
    1.20 -    # specifically handle 'SubProblem (undefined_, pbl, arglist)'
    1.21 +    # specifically handle 'SubProblem (undefined, pbl, arglist)'
    1.22      # ???
    1.23  .*)
    1.24  (*WN0509 TODO "ProtoPure" ... would be more consistent