src/HOL/SPARK/Examples/ROOT.ML
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 41561 d1318f3c86ba
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

use_thys
  ["Gcd/Greatest_Common_Divisor",

   "Liseq/Longest_Increasing_Subsequence",

   "RIPEMD-160/F",
   "RIPEMD-160/Hash",
   "RIPEMD-160/K_L",
   "RIPEMD-160/K_R",
   "RIPEMD-160/R_L",
   "RIPEMD-160/Round",
   "RIPEMD-160/R_R",
   "RIPEMD-160/S_L",
   "RIPEMD-160/S_R",

   "Sqrt/Sqrt"];