src/HOL/Codegenerator_Test/Candidates.thy
changeset 51160 599ff65b85e2
parent 49077 154f25a162e3
child 51161 6ed12ae3b3e1
equal deleted inserted replaced
51159:3fe7242f8346 51160:599ff65b85e2
     4 header {* A huge collection of equations to generate code from *}
     4 header {* A huge collection of equations to generate code from *}
     5 
     5 
     6 theory Candidates
     6 theory Candidates
     7 imports
     7 imports
     8   Complex_Main
     8   Complex_Main
     9   Library
     9   "~~/src/HOL/Library/Library"
    10   "~~/src/HOL/Library/Sublist"
    10   "~~/src/HOL/Library/Sublist"
    11   "~~/src/HOL/Number_Theory/Primes"
    11   "~~/src/HOL/Number_Theory/Primes"
    12   "~~/src/HOL/ex/Records"
    12   "~~/src/HOL/ex/Records"
    13 begin
    13 begin
    14 
    14