| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 11:02:32 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 37906 | e2b23ba9df13 |
| permissions | -rw-r--r-- |
| neuper@37906 | 1 |
(* equations and functions; functions NOT as lambda-terms |
| neuper@37906 | 2 |
author: Walther Neuper 2005, 2006 |
| neuper@37906 | 3 |
(c) due to copyright terms |
| neuper@37906 | 4 |
|
| neuper@37906 | 5 |
remove_thy"Equation"; |
| neuper@37906 | 6 |
use_thy"IsacKnowledge/Equation"; |
| neuper@37906 | 7 |
use_thy_only"IsacKnowledge/Equation"; |
| neuper@37906 | 8 |
|
| neuper@37906 | 9 |
remove_thy"Equation"; |
| neuper@37906 | 10 |
use_thy"IsacKnowledge/Isac"; |
| neuper@37906 | 11 |
*) |
| neuper@37906 | 12 |
|
| neuper@37906 | 13 |
Equation = Atools + |
| neuper@37906 | 14 |
|
| neuper@37906 | 15 |
consts |
| neuper@37906 | 16 |
|
| neuper@37906 | 17 |
(*descriptions in the related problems TODOshift here from Descriptions.thy*) |
| neuper@37906 | 18 |
substitution :: bool => una |
| neuper@37906 | 19 |
|
| neuper@37906 | 20 |
(*the CAS-commands*) |
| neuper@37906 | 21 |
solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *) |
| neuper@37906 | 22 |
solveTest :: "[bool * 'a] => bool list" (* for test collection *) |
| neuper@37906 | 23 |
|
| neuper@37906 | 24 |
(*Script-names*) |
| neuper@37906 | 25 |
Function2Equality :: "[bool, bool, bool] \ |
| neuper@37906 | 26 |
\=> bool" |
| neuper@37906 | 27 |
("((Script Function2Equality (_ _ =))// (_))" 9)
|
| neuper@37906 | 28 |
|
| neuper@37906 | 29 |
end |