equal
deleted
inserted
replaced
6 |
6 |
7 theory HOL |
7 theory HOL |
8 imports Pure "~~/src/Tools/Code_Generator" |
8 imports Pure "~~/src/Tools/Code_Generator" |
9 keywords |
9 keywords |
10 "try" "solve_direct" "quickcheck" |
10 "try" "solve_direct" "quickcheck" |
11 "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" |
11 "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and |
12 "print_case_translations":: diag and |
|
13 "quickcheck_params" :: thy_decl |
12 "quickcheck_params" :: thy_decl |
14 begin |
13 begin |
15 |
14 |
16 ML_file "~~/src/Tools/misc_legacy.ML" |
15 ML_file "~~/src/Tools/misc_legacy.ML" |
17 ML_file "~~/src/Tools/try.ML" |
16 ML_file "~~/src/Tools/try.ML" |