Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/ex/Codegenerator_Candidates.thy
changeset 36147 b43b22f63665
parent 36115 6601c227c5bf
child 36955 5fb251d1c32f
equal deleted inserted replaced
36146:7bfbb247a5df 36147:b43b22f63665 
    18   Option_ord
 
    18   Option_ord
 
    19   Permutation
 
    19   Permutation
 
    20   "~~/src/HOL/Number_Theory/Primes"
 
    20   "~~/src/HOL/Number_Theory/Primes"
 
    21   Product_ord
 
    21   Product_ord
 
    22   "~~/src/HOL/ex/Records"
 
    22   "~~/src/HOL/ex/Records"
 
       
    23   RBT
 
    23   SetsAndFunctions
 
    24   SetsAndFunctions
 
    24   Table
 
       
    25   While_Combinator
 
    25   While_Combinator
 
    26   Word
 
    26   Word
 
    27 begin
 
    27 begin
 
    28 
    28 
    29 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
 
    29 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
wneuper/isa