# HG changeset patch # User wenzelm # Date 1229374477 -3600 # Node ID 715178f6ae3127f12790c229797206c2d2c8b215 # Parent fb31b7a6c8582efdc3570437bc23ef0f12528710 repaired railroad accident; diff -r fb31b7a6c858 -r 715178f6ae31 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 15 21:41:21 2008 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 15 21:54:37 2008 +0100 @@ -812,6 +812,7 @@ 'sledgehammer' (nameref *) ; 'atp\_messages' ('(' nat ')')? + ; 'metis' thmrefs ;