--- a/src/HOL/HOL.thy Fri Apr 16 13:51:04 2004 +0200
+++ b/src/HOL/HOL.thy Fri Apr 16 13:52:43 2004 +0200
@@ -1022,15 +1022,13 @@
end); (* struct *)
-Context.>> (fn thy => (simpset_ref_of thy :=
- simpset_of thy
+simpset_ref() := simpset ()
addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
(* Adding the transitivity reasoners also as safe solvers showed a slight
speed up, but the reasoning strength appears to be not higher (at least
no breaking of additional proofs in the entire HOL distribution, as
of 5 March 2004, was observed). *)
- thy))
*}
(* Optional methods