src/HOL/Codegenerator_Test/Candidates.thy
changeset 49077 154f25a162e3
parent 41884 335895ffbd94
child 51160 599ff65b85e2
equal deleted inserted replaced
49073:88fe93ae61cf 49077:154f25a162e3
     5 
     5 
     6 theory Candidates
     6 theory Candidates
     7 imports
     7 imports
     8   Complex_Main
     8   Complex_Main
     9   Library
     9   Library
    10   "~~/src/HOL/Library/List_Prefix"
    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 
    15 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    15 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where