changeset 51673 | 4dfa00e264d8 |
parent 51314 | eac4bb5adbf9 |
child 51689 | 43a3465805dd |
--- a/src/HOL/HOL.thy Tue Jan 22 13:32:41 2013 +0100 +++ b/src/HOL/HOL.thy Tue Jan 22 14:33:45 2013 +0100 @@ -8,7 +8,8 @@ imports Pure "~~/src/Tools/Code_Generator" keywords "try" "solve_direct" "quickcheck" - "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and + "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" + "print_case_translations":: diag and "quickcheck_params" :: thy_decl begin