# HG changeset patch # User wenzelm # Date 1467384774 -7200 # Node ID 9321740ae1d4ac05dd29c3d94da739f9e4f93c6d # Parent d10eab0672f96bd79a6a06684a5b918201dca155 clarified; diff -r d10eab0672f9 -r 9321740ae1d4 src/HOL/Library/State_Monad.thy --- a/src/HOL/Library/State_Monad.thy Fri Jul 01 16:52:35 2016 +0200 +++ b/src/HOL/Library/State_Monad.thy Fri Jul 01 16:52:54 2016 +0200 @@ -145,7 +145,7 @@ "_sdo_block (_sdo_final e)" => "e" text \ - For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman.thy"}. + For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy"}. \ end