1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/Scripts/Isabelle-isac-conflicts	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,22 @@
     1.4 +6.8.02:
     1.5 +(1) special constants are already defined by Isabelle2002, 
     1.6 +    and thus cannot be parsed from terms; eg.
     1.7 +
     1.8 +    Reals		thus formula 'subproblem (Reals,...)' not possible
     1.9 +    power		thus 'Calculate power' not possible in Scripts
    1.10 +    
    1.11 +(2) numerals in (terms and) thms are stored differently:
    1.12 +    string	Isabelle term		isac term
    1.13 +    123		Bin....			Free("123",_)
    1.14 +    0		Const("0",_)		Free("0",_)
    1.15 +    0		Const("1",_)		Free("1",_)
    1.16 +
    1.17 +(3) overwritteln functions
    1.18 +    find_first		see isac/ROOT.ML
    1.19 +
    1.20 +
    1.21 +Questions for Isabelle team:
    1.22 +
    1.23 +28.02.03
    1.24 +(4)	what is going on in Isa02/Typefix.thy (Markus Wenzen) ?
    1.25 +(5)	how avoid "- x" ---parse--->  Free ("-x", _)  ?
    1.26 \ No newline at end of file