equal
deleted
inserted
replaced
97 different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
97 different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
98 examples. |
98 examples. |
99 |
99 |
100 |
100 |
101 *** HOL *** |
101 *** HOL *** |
|
102 |
|
103 * Command 'code_reflect' accepts empty constructor lists for datatypes, |
|
104 which renders those abstract effectively. |
102 |
105 |
103 * Probability/Random_Permutations.thy contains some theory about |
106 * Probability/Random_Permutations.thy contains some theory about |
104 choosing a permutation of a set uniformly at random and folding over a |
107 choosing a permutation of a set uniformly at random and folding over a |
105 list in random order. |
108 list in random order. |
106 |
109 |