src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 40137 9eabcb1bfe50
parent 40100 98d74bbe8cd8
child 40885 da4bdafeef7c
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Oct 25 21:17:11 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Oct 25 21:17:12 2010 +0200
     1.3 @@ -974,9 +974,10 @@
     1.4  
     1.5  code_pred [new_random_dseq inductify] avl .
     1.6  thm avl.new_random_dseq_equation
     1.7 +(* TODO: has highly non-deterministic execution time!
     1.8  
     1.9  values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
    1.10 -
    1.11 +*)
    1.12  fun set_of
    1.13  where
    1.14  "set_of ET = {}"