src/Tools/isac/Knowledge/Isac.thy
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37906 e2b23ba9df13
child 37954 4022d670753c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Isac.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,21 @@
     1.4 +(* theory collecting all knowledge defined so far
     1.5 +   WN.11.00
     1.6 + *)
     1.7 +
     1.8 +Isac = PolyMinus + PolyEq + Vect + DiffApp + Biegelinie + AlgEin
     1.9 +       + (*InsSort +*) Test + 
    1.10 +
    1.11 +end
    1.12 +
    1.13 +(* dependencies alternative to those defined by R.Lang during his thesis:
    1.14 +
    1.15 +   Poly				Root
    1.16 +     |\__________		 |
    1.17 +     |		 \ 		 |
    1.18 +     |		Rational	 |
    1.19 +     |		  |		 |
    1.20 +   PolyEq	RatEq		RootEq
    1.21 +      \         /  \           /
    1.22 +       \       /    \         /
    1.23 +	RatPolyEq    RatRootEq    etc.
    1.24 +*)