2 (1) special constants are already defined by Isabelle2002,
3 and thus cannot be parsed from terms; eg.
5 Reals thus formula 'subproblem (Reals,...)' not possible
6 power thus 'Calculate power' not possible in Scripts
8 (2) numerals in (terms and) thms are stored differently:
9 string Isabelle term isac term
10 123 Bin.... Free("123",_)
11 0 Const("0",_) Free("0",_)
12 0 Const("1",_) Free("1",_)
14 (3) overwritteln functions
15 find_first see isac/ROOT.ML
18 Questions for Isabelle team:
21 (4) what is going on in Isa02/Typefix.thy (Markus Wenzen) ?
22 (5) how avoid "- x" ---parse---> Free ("-x", _) ?