| author | agriesma |
| Thu, 17 Apr 2003 18:01:03 +0200 | |
| branch | griesmayer |
| changeset 320 | ed44605b37b6 |
| child 702 | 74da3871199d |
| permissions | -rw-r--r-- |
| agriesma@320 | 1 |
(* theory collecting all knowledge defined so far |
| agriesma@320 | 2 |
WN.11.00 |
| agriesma@320 | 3 |
*) |
| agriesma@320 | 4 |
|
| agriesma@320 | 5 |
Isac = Equation + PolyEq + Vect + DiffApp + Test + |
| agriesma@320 | 6 |
|
| agriesma@320 | 7 |
end |
| agriesma@320 | 8 |
|
| agriesma@320 | 9 |
(* dependencies alternative to those defined by R.Lang during his thesis: |
| agriesma@320 | 10 |
|
| agriesma@320 | 11 |
Poly Root |
| agriesma@320 | 12 |
|\__________ | |
| agriesma@320 | 13 |
| \ | |
| agriesma@320 | 14 |
| Rational | |
| agriesma@320 | 15 |
| | | |
| agriesma@320 | 16 |
PolyEq RatEq RootEq |
| agriesma@320 | 17 |
\ / \ / |
| agriesma@320 | 18 |
\ / \ / |
| agriesma@320 | 19 |
RatPolyEq RatRootEq etc. |
| agriesma@320 | 20 |
*) |
| agriesma@320 | 21 |
|
| agriesma@320 | 22 |
(* |
| agriesma@320 | 23 |
Isac = DiffAppl + InsSort + Rationals2 + Rationals + LinArith |
| agriesma@320 | 24 |
|
| agriesma@320 | 25 |
6.8.02 change to Isabelle2002 caused error -- thy excluded ! |
| agriesma@320 | 26 |
|
| agriesma@320 | 27 |
Proving equations for primrec function(s) "InsSort.foldr" ... |
| agriesma@320 | 28 |
GC #1.17.30.54.345.21479: (10 ms) |
| agriesma@320 | 29 |
*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list" |
| agriesma@320 | 30 |
*** imposes additional sort constraints on the declared type of the constant |
| agriesma@320 | 31 |
*** The error(s) above occurred in definition "InsSort.ins.ins_list_def" |
| agriesma@320 | 32 |
*) |
| agriesma@320 | 33 |