src/HOL/HOL.thy
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