# HG changeset patch # User wenzelm # Date 1299161960 -3600 # Node ID ae8d62656392e9115677b90d947dd0b8cc12e7e0 # Parent ea4d8dc12ed501113e08c198d0faeaab9aa9bb70 removed spurious 'unused_thms' (cf. 1a65b780bd56); diff -r ea4d8dc12ed5 -r ae8d62656392 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 15:18:05 2011 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 15:19:20 2011 +0100 @@ -5621,6 +5621,4 @@ apply mir done -unused_thms - end