1.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML	Sun Jan 06 18:56:55 2008 +0100
     1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML	Sun Jan 06 19:16:26 2008 +0100
     1.3 @@ -122,8 +122,11 @@
     1.4  
     1.5  
     1.6  	 Thm ("subtrahiere",num_str subtrahiere),
     1.7 -	 (*"[| l is_const; m is_const |] ==>  \
     1.8 -			    \m * v - l * v = (m - l) * v"*)
     1.9 +	 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
    1.10 +	 Thm ("subtrahiere_von_1",num_str subtrahiere_von_1),
    1.11 +	 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
    1.12 +	 Thm ("subtrahiere_1",num_str subtrahiere_1),
    1.13 +	 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
    1.14  
    1.15  	 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus), 
    1.16  	 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)

     2.1 --- a/src/sml/IsacKnowledge/PolyMinus.thy	Sun Jan 06 18:56:55 2008 +0100
     2.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy	Sun Jan 06 19:16:26 2008 +0100
     2.3 @@ -59,6 +59,11 @@
     2.4  
     2.5    subtrahiere               "[| l is_const; m is_const |] ==>  \
     2.6  			    \m * v - l * v = (m - l) * v"
     2.7 +  subtrahiere_von_1         "[| l is_const |] ==>  \
     2.8 +			    \v - l * v = (1 - l) * v"
     2.9 +  subtrahiere_1             "[| l is_const; m is_const |] ==>  \
    2.10 +			    \m * v - v = (m - 1) * v"
    2.11 +
    2.12    subtrahiere_x_plus_minus  "[| l is_const; m is_const |] ==>  \
    2.13  			    \(x + m * v) - l * v = x + (m - l) * v"
    2.14    subtrahiere_x_plus1_minus "[| l is_const |] ==>  \