equal
deleted
inserted
replaced
17 |
17 |
18 declare size_list_simps[code_pred_def] |
18 declare size_list_simps[code_pred_def] |
19 declare size_list_def[symmetric, code_pred_inline] |
19 declare size_list_def[symmetric, code_pred_inline] |
20 |
20 |
21 |
21 |
22 setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} |
22 setup {* |
|
23 Context.theory_map |
|
24 (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) |
|
25 *} |
23 |
26 |
24 datatype alphabet = a | b |
27 datatype alphabet = a | b |
25 |
28 |
26 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
29 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
27 "[] \<in> S\<^isub>1" |
30 "[] \<in> S\<^isub>1" |