equal
deleted
inserted
replaced
1 (* equations and functions; functions NOT as lambda-terms |
|
2 author: Walther Neuper 2005, 2006 |
|
3 (c) due to copyright terms |
|
4 |
|
5 remove_thy"Equation"; |
|
6 use_thy"IsacKnowledge/Equation"; |
|
7 use_thy_only"IsacKnowledge/Equation"; |
|
8 |
|
9 remove_thy"Equation"; |
|
10 use_thy"IsacKnowledge/Isac"; |
|
11 *) |
|
12 |
|
13 Equation = Atools + |
|
14 |
|
15 consts |
|
16 |
|
17 (*descriptions in the related problems TODOshift here from Descriptions.thy*) |
|
18 substitution :: bool => una |
|
19 |
|
20 (*the CAS-commands*) |
|
21 solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *) |
|
22 solveTest :: "[bool * 'a] => bool list" (* for test collection *) |
|
23 |
|
24 (*Script-names*) |
|
25 Function2Equality :: "[bool, bool, bool] \ |
|
26 \=> bool" |
|
27 ("((Script Function2Equality (_ _ =))// (_))" 9) |
|
28 |
|
29 end |
|