changeset 2563 | e908e2716f3a |
parent 2326 | 6df4488339e4 |
child 3511 | da4dd8b7ced4 |
--- 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";