| author | Walther Neuper <neuper@ist.tugraz.at> |
| Wed, 21 Jul 2010 13:53:39 +0200 | |
| branch | isac-from-Isabelle2009-2 |
| changeset 37871 | 875b6efa7ced |
| permissions | -rw-r--r-- |
| neuper@37871 | 1 |
6.8.02: |
| neuper@37871 | 2 |
(1) special constants are already defined by Isabelle2002, |
| neuper@37871 | 3 |
and thus cannot be parsed from terms; eg. |
| neuper@37871 | 4 |
|
| neuper@37871 | 5 |
Reals thus formula 'subproblem (Reals,...)' not possible |
| neuper@37871 | 6 |
power thus 'Calculate power' not possible in Scripts |
| neuper@37871 | 7 |
|
| neuper@37871 | 8 |
(2) numerals in (terms and) thms are stored differently: |
| neuper@37871 | 9 |
string Isabelle term isac term |
| neuper@37871 | 10 |
123 Bin.... Free("123",_)
|
| neuper@37871 | 11 |
0 Const("0",_) Free("0",_)
|
| neuper@37871 | 12 |
0 Const("1",_) Free("1",_)
|
| neuper@37871 | 13 |
|
| neuper@37871 | 14 |
(3) overwritteln functions |
| neuper@37871 | 15 |
find_first see isac/ROOT.ML |
| neuper@37871 | 16 |
|
| neuper@37871 | 17 |
|
| neuper@37871 | 18 |
Questions for Isabelle team: |
| neuper@37871 | 19 |
|
| neuper@37871 | 20 |
28.02.03 |
| neuper@37871 | 21 |
(4) what is going on in Isa02/Typefix.thy (Markus Wenzen) ? |
| neuper@37871 | 22 |
(5) how avoid "- x" ---parse---> Free ("-x", _) ? |