removed assignment of HOL_ss to simpset
authorclasohm
Fri, 19 Apr 1996 11:13:05 +0200
changeset 1666 5183de4c496d
parent 1665 e5737154d9bf
child 1667 6056e9c967d9
removed assignment of HOL_ss to simpset
src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Apr 19 11:12:05 1996 +0200
+++ b/src/HOL/Fun.ML	Fri Apr 19 11:13:05 1996 +0200
@@ -6,8 +6,6 @@
 Lemmas about functions.
 *)
 
-simpset := HOL_ss;
-
 goal Fun.thy "(f = g) = (!x. f(x)=g(x))";
 by (rtac iffI 1);
 by (Asm_simp_tac 1);