src/ZF/Order.ML
changeset 7570 a9391550eea1
parent 7499 23e090051cb8
child 8201 a81d18b0a9b1
     1.1 --- a/src/ZF/Order.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/ZF/Order.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -242,9 +242,9 @@
     1.4  
     1.5  (*Rewriting with bijections and converse (function inverse)*)
     1.6  val bij_inverse_ss = 
     1.7 -    simpset() setSolver 
     1.8 -      type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
     1.9 -				       inj_is_fun, comp_fun, comp_bij])
    1.10 +    simpset() setSolver (mk_solver ""
    1.11 +      (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
    1.12 +				        inj_is_fun, comp_fun, comp_bij])))
    1.13            addsimps [right_inverse_bij];
    1.14  
    1.15  Goalw [ord_iso_def]