author | paulson |
Wed, 29 Jan 1997 15:34:23 +0100 | |
changeset 2563 | e908e2716f3a |
parent 2562 | d571d6660240 |
child 2564 | 9d66b758bce5 |
--- a/src/HOL/Auth/DB-ROOT.ML Wed Jan 29 15:32:18 1997 +0100 +++ b/src/HOL/Auth/DB-ROOT.ML Wed Jan 29 15:34:23 1997 +0100 @@ -14,11 +14,5 @@ init_thy_reader(); -(*Must be redefined in order to refer to the new instance of bind_thm - created by init_thy_reader.*) -fun qed_spec_mp name = - let val thm = normalize_thm [RSspec,RSmp] (result()) - in bind_thm(name, thm) end; - use_thy "Message";