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