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