1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -257,7 +257,7 @@
1.4 (* FIXME: Division von x^9+x^5+1 durch x-1000 funktioniert nicht,
1.5 integer zu klein *)
1.6 fun uv_mod_pdiv (p1:uv_poly) ([]:uv_poly) =
1.7 - raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")
1.8 + error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero")
1.9 | uv_mod_pdiv p1 [x] =
1.10 let
1.11 val xs= Unsynchronized.ref [];
1.12 @@ -267,7 +267,7 @@
1.13 xs:=(uv_mod_rem_poly(p1,x));
1.14 while length(!xs)>0 andalso hd(!xs)=0 do xs:=tl(!xs)
1.15 )
1.16 - else raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero");
1.17 + else error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: division by zero");
1.18 ([]:uv_poly,!xs:uv_poly)
1.19 end
1.20 | uv_mod_pdiv p1 p2 =
1.21 @@ -283,7 +283,7 @@
1.22 in
1.23 (
1.24 if (!m)=0 orelse p2=[0]
1.25 - then raise error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: Division by zero")
1.26 + then error ("RATIONALS_UV_MOD_PDIV_EXCEPTION: Division by zero")
1.27 else
1.28 (
1.29 if (!m)<n then
1.30 @@ -323,7 +323,7 @@
1.31 val output= Unsynchronized.ref ([],[]);
1.32 in
1.33 (
1.34 - if (!m)=0 orelse p2=[0] then raise error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")
1.35 + if (!m)=0 orelse p2=[0] then error ("RATIONALS_UV_MOD_PDIVP_EXCEPTION: Division by zero")
1.36 else
1.37 (
1.38 if (!m)<n then
1.39 @@ -354,12 +354,12 @@
1.40 end;
1.41
1.42 (*. calculates the remainder of p1/p2 .*)
1.43 -fun uv_mod_prest (p1:uv_poly) ([]:uv_poly) = raise error("UV_MOD_PREST_EXCEPTION: Division by zero")
1.44 +fun uv_mod_prest (p1:uv_poly) ([]:uv_poly) = error("UV_MOD_PREST_EXCEPTION: Division by zero")
1.45 | uv_mod_prest [] p2 = []:uv_poly
1.46 | uv_mod_prest p1 p2 = (#2(uv_mod_pdiv p1 p2));
1.47
1.48 (*. calculates the remainder of p1/p2 in Zp .*)
1.49 -fun uv_mod_prestp (p1:uv_poly) ([]:uv_poly) p= raise error("UV_MOD_PRESTP_EXCEPTION: Division by zero")
1.50 +fun uv_mod_prestp (p1:uv_poly) ([]:uv_poly) p= error("UV_MOD_PRESTP_EXCEPTION: Division by zero")
1.51 | uv_mod_prestp [] p2 p= []:uv_poly
1.52 | uv_mod_prestp p1 p2 p = #2(uv_mod_pdivp p1 p2 p);
1.53
1.54 @@ -368,7 +368,7 @@
1.55 | uv_mod_cont (x::p)= gcd_int x (uv_mod_cont(p));
1.56
1.57 (*. divides each coefficient of a uv polynomial by y .*)
1.58 -fun uv_mod_div_list (p:uv_poly,0) = raise error("UV_MOD_DIV_LIST_EXCEPTION: Division by zero")
1.59 +fun uv_mod_div_list (p:uv_poly,0) = error("UV_MOD_DIV_LIST_EXCEPTION: Division by zero")
1.60 | uv_mod_div_list ([],y) = []:uv_poly
1.61 | uv_mod_div_list (x::p,y) = (x div y)::uv_mod_div_list(p,y);
1.62
1.63 @@ -381,7 +381,7 @@
1.64 (
1.65 c:=uv_mod_cont(p);
1.66
1.67 - if !c=0 then raise error ("RATIONALS_UV_MOD_PP_EXCEPTION: content is 0")
1.68 + if !c=0 then error ("RATIONALS_UV_MOD_PP_EXCEPTION: content is 0")
1.69 else uv_mod_div_list(p,!c)
1.70 )
1.71 end;
1.72 @@ -517,11 +517,11 @@
1.73 end;
1.74
1.75 (*. decides if p1 is a factor of p2 in Zp .*)
1.76 -fun uv_mod_dividesp ([]:uv_poly) (p2:uv_poly) p= raise error("UV_MOD_DIVIDESP: Division by zero")
1.77 +fun uv_mod_dividesp ([]:uv_poly) (p2:uv_poly) p= error("UV_MOD_DIVIDESP: Division by zero")
1.78 | uv_mod_dividesp p1 p2 p= if uv_mod_prestp p2 p1 p = [] then true else false;
1.79
1.80 (*. decides if p1 is a factor of p2 .*)
1.81 -fun uv_mod_divides ([]:uv_poly) (p2:uv_poly) = raise error("UV_MOD_DIVIDES: Division by zero")
1.82 +fun uv_mod_divides ([]:uv_poly) (p2:uv_poly) = error("UV_MOD_DIVIDES: Division by zero")
1.83 | uv_mod_divides p1 p2 = if uv_mod_prest p2 p1 = [] then true else false;
1.84
1.85 (*. chinese remainder algorithm .*)
1.86 @@ -545,8 +545,8 @@
1.87
1.88 (*. applies the chinese remainder algorithmen to the coefficients of x1 and x2 .*)
1.89 fun uv_mod_cra_2 ([],[],m1,m2) = []
1.90 - | uv_mod_cra_2 ([],x2,m1,m2) = raise error("UV_MOD_CRA_2_EXCEPTION: invalid call x1")
1.91 - | uv_mod_cra_2 (x1,[],m1,m2) = raise error("UV_MOD_CRA_2_EXCEPTION: invalid call x2")
1.92 + | uv_mod_cra_2 ([],x2,m1,m2) = error("UV_MOD_CRA_2_EXCEPTION: invalid call x1")
1.93 + | uv_mod_cra_2 (x1,[],m1,m2) = error("UV_MOD_CRA_2_EXCEPTION: invalid call x2")
1.94 | uv_mod_cra_2 (x1::x1s,x2::x2s,m1,m2) = (uv_mod_cra2(x1,x2,m1,m2))::(uv_mod_cra_2(x1s,x2s,m1,m2));
1.95
1.96 (*. calculates the gcd of two uv polynomials p1' and p2' with the modular algorithm .*)
1.97 @@ -688,18 +688,18 @@
1.98 fun mv_monom_greater((M1x,M1l):mv_monom,(M2x,M2l):mv_monom,order)=
1.99 if order=LEX_ then
1.100 (
1.101 - if length(M1l)<>length(M2l) then raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
1.102 + if length(M1l)<>length(M2l) then error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
1.103 else if (mv_mg_hlp((map op- (M1l~~M2l)))<>GREATER) then false else true
1.104 )
1.105 else
1.106 if order=GGO_ then
1.107 (
1.108 - if length(M1l)<>length(M2l) then raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
1.109 + if length(M1l)<>length(M2l) then error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Order error")
1.110 else
1.111 if mv_addlist(M1l)=mv_addlist(M2l) then if (mv_mg_hlp((map op- (M1l~~M2l)))<>GREATER) then false else true
1.112 else if mv_addlist(M1l)>mv_addlist(M2l) then true else false
1.113 )
1.114 - else raise error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Wrong Order");
1.115 + else error ("RATIONALS_MV_MONOM_GREATER_EXCEPTION: Wrong Order");
1.116
1.117 (*. tests if the monomial X is greater as the monomial Y and returns a order value (GREATER,EQUAL,LESS) .*)
1.118 (*. 2 orders are implemented LEX_/GGO_ (lexigraphical/greatest degree order) .*)
1.119 @@ -710,7 +710,7 @@
1.120 if order=LEX_ then
1.121 (
1.122 if length(x)<>length(y) then
1.123 - raise error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
1.124 + error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
1.125 else
1.126 (
1.127 temp:=mv_mg_hlp((map op- (x~~y)));
1.128 @@ -726,18 +726,18 @@
1.129 if order=GGO_ then
1.130 (
1.131 if length(x)<>length(y) then
1.132 - raise error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
1.133 + error ("RATIONALS_MV_GEQ_EXCEPTION: Order error")
1.134 else
1.135 if mv_addlist(x)=mv_addlist(y) then
1.136 (mv_mg_hlp((map op- (x~~y))))
1.137 else if mv_addlist(x)>mv_addlist(y) then GREATER else LESS
1.138 )
1.139 - else raise error ("RATIONALS_MV_GEQ_EXCEPTION: Wrong Order")
1.140 + else error ("RATIONALS_MV_GEQ_EXCEPTION: Wrong Order")
1.141 end;
1.142
1.143 (*. cuts the first variable from a polynomial .*)
1.144 fun mv_cut([]:mv_poly)=[]:mv_poly
1.145 - | mv_cut((x,[])::list) = raise error ("RATIONALS_MV_CUT_EXCEPTION: Invalid list ")
1.146 + | mv_cut((x,[])::list) = error ("RATIONALS_MV_CUT_EXCEPTION: Invalid list ")
1.147 | mv_cut((x,y::ys)::list)=(x,ys)::mv_cut(list);
1.148
1.149 (*. leading power product .*)
1.150 @@ -775,7 +775,7 @@
1.151 lc:=hd(mv_cut([hd(!p1o)]))::(!lc);
1.152 p1o:=tl(!p1o)
1.153 );
1.154 - if !lc=[] then raise error ("RATIONALS_MV_LC_EXCEPTION: lc is empty") else ();
1.155 + if !lc=[] then error ("RATIONALS_MV_LC_EXCEPTION: lc is empty") else ();
1.156 mv_rev_to(!lc)
1.157 )
1.158 end;
1.159 @@ -848,14 +848,14 @@
1.160
1.161 (*. division of monomials .*)
1.162 fun mv_mdiv((0,[]):mv_monom,_:mv_monom)=(0,[]):mv_monom
1.163 - | mv_mdiv(_,(0,[]))= raise error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")
1.164 + | mv_mdiv(_,(0,[]))= error ("RATIONALS_MV_MDIV_EXCEPTION Division by 0 ")
1.165 | mv_mdiv(p1:mv_monom,p2:mv_monom)=
1.166 let
1.167 val c= Unsynchronized.ref (#1(p2));
1.168 val pp= Unsynchronized.ref [];
1.169 in
1.170 (
1.171 - if !c=0 then raise error("MV_MDIV_EXCEPTION Dividing by zero")
1.172 + if !c=0 then error("MV_MDIV_EXCEPTION Dividing by zero")
1.173 else c:=(#1(p1) div #1(p2));
1.174 if #1(p2)<>0 then
1.175 (
1.176 @@ -863,7 +863,7 @@
1.177 if mv_is_negativ(!pp) then (0,!pp)
1.178 else (!c,!pp)
1.179 )
1.180 - else raise error("MV_MDIV_EXCEPTION Dividing by empty Polynom")
1.181 + else error("MV_MDIV_EXCEPTION Dividing by empty Polynom")
1.182 )
1.183 end;
1.184
1.185 @@ -875,7 +875,7 @@
1.186
1.187 (*. division of two multivariate polynomials .*)
1.188 fun mv_division([]:mv_poly,g:mv_poly,order)=([]:mv_poly,[]:mv_poly)
1.189 - | mv_division(f,[],order)= raise error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
1.190 + | mv_division(f,[],order)= error ("RATIONALS_MV_DIVISION_EXCEPTION Division by zero")
1.191 | mv_division(f,g,order)=
1.192 let
1.193 val r= Unsynchronized.ref [];
1.194 @@ -887,7 +887,7 @@
1.195 in
1.196 r := rev(sort (mv_geq order) (mv_shorten(f,order)));
1.197 g':= rev(sort (mv_geq order) (mv_shorten(g,order)));
1.198 - if #1(hd(!g'))=0 then raise error("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero") else ();
1.199 + if #1(hd(!g'))=0 then error("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero") else ();
1.200 if (mv_monom_greater (hd(!g'),hd(!r),order)) then ([(0,mv_null2(#2(hd(f))))],(!r))
1.201 else
1.202 (
1.203 @@ -895,7 +895,7 @@
1.204 while (if (!exit)=0 then not(mv_monom_greater (hd(!g'),hd(!r),order)) else false) do
1.205 (
1.206 if (#1(mv_lm(!g',order)))<>0 then m:=mv_mdiv(mv_lm(!r,order),mv_lm(!g',order))
1.207 - else raise error ("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero");
1.208 + else error ("RATIONALS_MV_DIVISION_EXCEPTION: Dividing by zero");
1.209 if #1(!m)<>0 then
1.210 (
1.211 q:=(!m)::(!q);
1.212 @@ -920,8 +920,8 @@
1.213 (*. multivariate case .*)
1.214
1.215 (*. decides if x is a factor of y .*)
1.216 -fun mv_divides([]:mv_poly,[]:mv_poly)= raise error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
1.217 - | mv_divides(x,[]) = raise error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
1.218 +fun mv_divides([]:mv_poly,[]:mv_poly)= error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
1.219 + | mv_divides(x,[]) = error("RATIONALS_MV_DIVIDES_EXCEPTION: division by zero")
1.220 | mv_divides(x:mv_poly,y:mv_poly) = #2(mv_division(y,x,LEX_))=[];
1.221
1.222 (*. gets the maximum of a and b .*)
1.223 @@ -964,7 +964,7 @@
1.224 val help= Unsynchronized.ref ((c1,e1)::others);
1.225 val list= Unsynchronized.ref [];
1.226 in
1.227 - if length(e1)>1 then raise error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")
1.228 + if length(e1)>1 then error ("RATIONALS_TO_LIST_EXCEPTION: not univariate")
1.229 else if length(e1)=0 then [c1]
1.230 else
1.231 (
1.232 @@ -1176,7 +1176,7 @@
1.233 cont:=mv_content(p1);
1.234 pp:=(#1(mv_division(p1,!cont,LEX_)));
1.235 if !pp=[]
1.236 - then raise error("RATIONALS_MV_PP_EXCEPTION: Invalid Content ")
1.237 + then error("RATIONALS_MV_PP_EXCEPTION: Invalid Content ")
1.238 else (!pp)
1.239 end
1.240
1.241 @@ -1426,7 +1426,7 @@
1.242 );
1.243 SOME [(1,rev(!vl))] handle _ => NONE
1.244 )
1.245 - else raise error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")
1.246 + else error ("RATIONALS_TERM2COEF_EXCEPTION 1: Invalid term")
1.247 )
1.248 end
1.249 | term2coef' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option=
1.250 @@ -1437,7 +1437,7 @@
1.251 (
1.252 SOME ((the(term2coef' t1 v)) @ mv_skalar_mul((the(term2coef' t2 v)),1)) handle _ => NONE
1.253 )
1.254 - | term2coef' (term) v = raise error ("RATIONALS_TERM2COEF_EXCEPTION 2: Invalid term");
1.255 + | term2coef' (term) v = error ("RATIONALS_TERM2COEF_EXCEPTION 2: Invalid term");
1.256
1.257 (*. checks if all coefficients of a polynomial are positiv (except the first) .*)
1.258 fun check_coeff t = (* erste Koeffizient kann <0 sein !!! *)
1.259 @@ -1541,7 +1541,7 @@
1.260 );
1.261 SOME [(1,rev(!vl))] handle _ => NONE
1.262 )
1.263 - else raise error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")
1.264 + else error ("RATIONALS_TERM2POLY_EXCEPTION 1: Invalid term")
1.265 )
1.266 end
1.267 | term2poly' (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v :mv_poly option =
1.268 @@ -1552,7 +1552,7 @@
1.269 (
1.270 SOME ((the(term2poly' t1 v)) @ mv_skalar_mul((the(term2poly' t2 v)),~1)) handle _ => NONE
1.271 )
1.272 - | term2poly' (term) v = raise error ("RATIONALS_TERM2POLY_EXCEPTION 2: Invalid term");
1.273 + | term2poly' (term) v = error ("RATIONALS_TERM2POLY_EXCEPTION 2: Invalid term");
1.274
1.275 (*. translates an Isabelle term into internal representation.
1.276 term2poly
1.277 @@ -1564,7 +1564,7 @@
1.278 .*)
1.279 fun term2poly (t:term) v =
1.280 if is_polynomial t then term2poly' t v
1.281 - else raise error ("term2poly: invalid = "^(term2str t));
1.282 + else error ("term2poly: invalid = "^(term2str t));
1.283
1.284 (*. same as term2poly with automatic detection of the variables .*)
1.285 fun term2polyx t = term2poly t (((map free2str) o vars) t);
1.286 @@ -1572,7 +1572,7 @@
1.287 (*. checks if the term is in expanded polynomial form and converts it into the internal representation .*)
1.288 fun expanded2poly (t:term) v =
1.289 (*if is_expanded t then*) term2poly' t v
1.290 - (*else raise error ("RATIONALS_EXPANDED2POLY_EXCEPTION: Invalid Polynomial")*);
1.291 + (*else error ("RATIONALS_EXPANDED2POLY_EXCEPTION: Invalid Polynomial")*);
1.292
1.293 (*. same as expanded2poly with automatic detection of the variables .*)
1.294 fun expanded2polyx t = expanded2poly t (((map free2str) o vars) t);
1.295 @@ -1804,7 +1804,7 @@
1.296 )
1.297 )
1.298 end
1.299 -| step_cancel _ = raise error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
1.300 +| step_cancel _ = error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
1.301
1.302
1.303 (*. same as step_cancel, this time for expanded forms (input+output) .*)
1.304 @@ -1869,7 +1869,7 @@
1.305 )
1.306 )
1.307 end
1.308 -| step_cancel_expanded _ = raise error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
1.309 +| step_cancel_expanded _ = error ("RATIONALS_STEP_CANCEL_EXCEPTION: Invalid fraction");
1.310
1.311 (*. calculates the greatest common divisor of numerator and denominator and divides each through it .*)
1.312 fun direct_cancel (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
1.313 @@ -1954,7 +1954,7 @@
1.314 )
1.315 )
1.316 end
1.317 - | direct_cancel _ = raise error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
1.318 + | direct_cancel _ = error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
1.319
1.320 (*. same es direct_cancel, this time for expanded forms (input+output).*)
1.321 fun direct_cancel_expanded (t as Const ("Rings.inverse_class.divide",_) $ p1 $ p2) =
1.322 @@ -2039,7 +2039,7 @@
1.323 )
1.324 )
1.325 end
1.326 - | direct_cancel_expanded _ = raise error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
1.327 + | direct_cancel_expanded _ = error ("RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction");
1.328
1.329
1.330 (*. adds two fractions .*)
1.331 @@ -2086,7 +2086,7 @@
1.332 )
1.333 )
1.334 end
1.335 - | add_fract (_,_) = raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
1.336 + | add_fract (_,_) = error ("RATIONALS_ADD_FRACTION_EXCEPTION: Invalid add_fraction call");
1.337
1.338 (*. adds two expanded fractions .*)
1.339 fun add_fract_exp ((Const("Rings.inverse_class.divide",_) $ t11 $ t12),(Const("Rings.inverse_class.divide",_) $ t21 $ t22)) =
1.340 @@ -2120,7 +2120,7 @@
1.341 )
1.342 )
1.343 end
1.344 - | add_fract_exp (_,_) = raise error ("RATIONALS_ADD_FRACTION_EXP_EXCEPTION: Invalid add_fraction call");
1.345 + | add_fract_exp (_,_) = error ("RATIONALS_ADD_FRACTION_EXP_EXCEPTION: Invalid add_fraction call");
1.346
1.347 (*. adds a list of terms .*)
1.348 fun add_list_of_fractions []= (Free("0",HOLogic.realT),[])
1.349 @@ -2576,7 +2576,7 @@
1.350 if last=[(1,mv_null2(vars))] then make_term(factor_list,vars)
1.351 else make_term(last::factor_list,vars)
1.352 )
1.353 - else raise error ("RATIONALS_FACTORIZE_DEN_EXCEPTION: Invalid factor by division")
1.354 + else error ("RATIONALS_FACTORIZE_DEN_EXCEPTION: Invalid factor by division")
1.355 end;
1.356
1.357 (*. makes a term out of the elements of the list (expanded polynomial representation) .*)
1.358 @@ -2601,14 +2601,14 @@
1.359 if last=[(1,mv_null2(vars))] then make_exp(factor_list,vars)
1.360 else make_exp(last::factor_list,vars)
1.361 )
1.362 - else raise error ("RATIONALS_FACTORIZE_DEN_EXP_EXCEPTION: Invalid factor by division")
1.363 + else error ("RATIONALS_FACTORIZE_DEN_EXP_EXCEPTION: Invalid factor by division")
1.364 end;
1.365
1.366 (*. calculates the common denominator of all elements of the list and multiplies .*)
1.367 (*. the nominators and denominators with the correct factor .*)
1.368 (*. (polynomial representation) .*)
1.369 fun step_add_list_of_fractions []=(Free("0",HOLogic.realT),[]:term list)
1.370 - | step_add_list_of_fractions [x]= raise error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXCEPTION: Nothing to add")
1.371 + | step_add_list_of_fractions [x]= error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXCEPTION: Nothing to add")
1.372 | step_add_list_of_fractions (xs) =
1.373 let
1.374 val den_list=termlist2denominators (xs); (* list of denominators *)
1.375 @@ -2622,7 +2622,7 @@
1.376 (*. the nominators and denominators with the correct factor .*)
1.377 (*. (expanded polynomial representation) .*)
1.378 fun step_add_list_of_fractions_exp [] = (Free("0",HOLogic.realT),[]:term list)
1.379 - | step_add_list_of_fractions_exp [x] = raise error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXP_EXCEPTION: Nothing to add")
1.380 + | step_add_list_of_fractions_exp [x] = error ("RATIONALS_STEP_ADD_LIST_OF_FRACTIONS_EXP_EXCEPTION: Nothing to add")
1.381 | step_add_list_of_fractions_exp (xs)=
1.382 let
1.383 val den_list=termlist2denominators_exp (xs); (* list of denominators *)
1.384 @@ -2688,8 +2688,8 @@
1.385 ]
1.386 | term2list (Const("Groups.plus_class.plus",_) $ t1 $ t2) = term2list(t1) @ term2list(t2)
1.387 | term2list (Const("Groups.minus_class.minus",_) $ t1 $ t2) =
1.388 - raise error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
1.389 - | term2list _ = raise error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");
1.390 + error ("RATIONALS_TERM2LIST_EXCEPTION: - not implemented yet")
1.391 + | term2list _ = error ("RATIONALS_TERM2LIST_EXCEPTION: invalid term");
1.392
1.393 (*.factors out the gcd of nominator and denominator:
1.394 a/b = (a' * gcd)/(b' * gcd), a,b,gcd are poly[2].*)
1.395 @@ -2732,7 +2732,7 @@
1.396 (let val ts = term2list t
1.397 in if 1 < length ts
1.398 then SOME (add_list_of_fractions ts)
1.399 - else NONE (*raise error ("RATIONALS_ADD_EXCEPTION: nothing to add")*)
1.400 + else NONE (*error ("RATIONALS_ADD_EXCEPTION: nothing to add")*)
1.401 end) handle _ => NONE
1.402 );
1.403 (*.same as add_fraction_p_ but with normalform [3].*)
1.404 @@ -2740,12 +2740,12 @@
1.405 fun add_fraction_ (thy:theory) t =
1.406 if length(term2list(t))>1
1.407 then SOME (add_list_of_fractions_exp(term2list(t))) handle _ => NONE
1.408 - else (*raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
1.409 + else (*error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
1.410 NONE;
1.411 fun add_fraction_ (thy:theory) t =
1.412 (if 1 < length (term2list t)
1.413 then SOME (add_list_of_fractions_exp (term2list t))
1.414 - else (*raise error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
1.415 + else (*error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
1.416 NONE) handle _ => NONE;
1.417
1.418 (*SOME (step_add_list_of_fractions2_exp(term2list(t))); *)
1.419 @@ -2947,7 +2947,7 @@
1.420 []) end
1.421 else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
1.422 | locate_rule _ _ _ _ _ _ =
1.423 - raise error ("locate_rule: doesnt match rev-sets in istate");
1.424 + error ("locate_rule: doesnt match rev-sets in istate");
1.425
1.426 (*.next_rule = fn : rule list -> term -> rule option
1.427 for a given term return the next rules to be done for cancelling.
1.428 @@ -2975,7 +2975,7 @@
1.429 | _ => NONE
1.430 end
1.431 | next_rule _ _ _ _ _ =
1.432 - raise error ("next_rule: doesnt match rev-sets in istate");
1.433 + error ("next_rule: doesnt match rev-sets in istate");
1.434
1.435 (*.val attach_form = f : rule list -> term -> term
1.436 -> (rule * (term * term list)) list
1.437 @@ -3054,7 +3054,7 @@
1.438 []) end
1.439 else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
1.440 | locate_rule _ _ _ _ _ _ =
1.441 - raise error ("locate_rule: doesnt match rev-sets in istate");
1.442 + error ("locate_rule: doesnt match rev-sets in istate");
1.443
1.444 fun next_rule thy eval_rls ro [rs] t =
1.445 let val der = make_deriv thy eval_rls rs ro NONE t;
1.446 @@ -3065,7 +3065,7 @@
1.447 | _ => NONE
1.448 end
1.449 | next_rule _ _ _ _ _ =
1.450 - raise error ("next_rule: doesnt match rev-sets in istate");
1.451 + error ("next_rule: doesnt match rev-sets in istate");
1.452
1.453 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1.454 []:(rule * (term * term list)) list;
1.455 @@ -3171,7 +3171,7 @@
1.456 []) end
1.457 else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
1.458 | locate_rule _ _ _ _ _ _ =
1.459 - raise error ("locate_rule: doesnt match rev-sets in istate");
1.460 + error ("locate_rule: doesnt match rev-sets in istate");
1.461
1.462 (*.next_rule = fn : rule list -> term -> rule option
1.463 for a given term return the next rules to be done for cancelling.
1.464 @@ -3199,7 +3199,7 @@
1.465 | _ => NONE
1.466 end
1.467 | next_rule _ _ _ _ _ =
1.468 - raise error ("next_rule: doesnt match rev-sets in istate");
1.469 + error ("next_rule: doesnt match rev-sets in istate");
1.470
1.471 (*.val attach_form = f : rule list -> term -> term
1.472 -> (rule * (term * term list)) list
1.473 @@ -3315,7 +3315,7 @@
1.474 []) end
1.475 else (tracing("### locate_rule: "^(id_of_thm r)^" not mem rrls");[])
1.476 | locate_rule _ _ _ _ _ _ =
1.477 - raise error ("locate_rule: doesnt match rev-sets in istate");
1.478 + error ("locate_rule: doesnt match rev-sets in istate");
1.479
1.480 (*.next_rule = fn : rule list -> term -> rule option
1.481 for a given term return the next rules to be done for cancelling.
1.482 @@ -3343,7 +3343,7 @@
1.483 | _ => NONE
1.484 end
1.485 | next_rule _ _ _ _ _ =
1.486 - raise error ("next_rule: doesnt match rev-sets in istate");
1.487 + error ("next_rule: doesnt match rev-sets in istate");
1.488
1.489 (*.val attach_form = f : rule list -> term -> term
1.490 -> (rule * (term * term list)) list