1.1 --- a/src/Tools/isac/Scripts/Isabelle-isac-conflicts	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,22 +0,0 @@
     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