# HG changeset patch # User haftmann # Date 1442916625 -7200 # Node ID 19ee25fe9737184de76be13b201ae089e22fb83a # Parent af7bed1360f30bf027054db921ee7f7d150dc5a1 include some data structures into code generation diff -r af7bed1360f3 -r 19ee25fe9737 src/HOL/Codegenerator_Test/Candidates.thy --- a/src/HOL/Codegenerator_Test/Candidates.thy Tue Sep 22 11:48:22 2015 +0200 +++ b/src/HOL/Codegenerator_Test/Candidates.thy Tue Sep 22 12:10:25 2015 +0200 @@ -8,6 +8,8 @@ Complex_Main "~~/src/HOL/Library/Library" "~~/src/HOL/Library/Sublist_Order" + "~~/src/HOL/Data_Structures/Tree_Map" + "~~/src/HOL/Data_Structures/Tree_Set" "~~/src/HOL/Number_Theory/Eratosthenes" "~~/src/HOL/ex/Records" begin