1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Jul 30 16:41:08 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Jul 31 15:16:47 2012 +0200
     1.3 @@ -187,7 +187,7 @@
     1.4  				   (*2nd NTH_CONS pushes n+-1 into asms*)
     1.5  				   Calc("Groups.plus_class.plus", eval_binop "#add_")
     1.6  				   ], 
     1.7 -		srls = Erls, calc = [],
     1.8 +		srls = Erls, calc = [], errpatts = [],
     1.9  		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.10  			 Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.11  			 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.12 @@ -208,7 +208,7 @@
    1.13  			    (*2nd NTH_CONS pushes n+-1 into asms*)
    1.14  			    Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.15  			    ], 
    1.16 -	 srls = Erls, calc = [],
    1.17 +	 srls = Erls, calc = [], errpatts = [],
    1.18  	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.19  		  Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.20  		  Thm ("NTH_NIL", num_str @{thm NTH_NIL}),