# HG changeset patch
# User wenzelm
# Date 1228335758 -3600
# Node ID da6c224a06e66833b5adfc8faa7efd658c74a4f0
# Parent  64754369cee36e0003700d9f3b896ad0fc6c9407
sources are not executable;

diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/KerberosIV_Gets.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/KerberosV.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/Kerberos_BAN_Gets.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/OtwayReesBella.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/Smartcard/EventSC.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/Smartcard/ShoupRubin.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/Smartcard/ShoupRubinBella.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Auth/Smartcard/Smartcard.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Library/BigO.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Library/Ramsey.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Library/SetsAndFunctions.thy
diff -r 64754369cee3 -r da6c224a06e6 src/HOL/Tools/res_reconstruct.ML