1.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 17:45:54 2012 +0100
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 19:02:34 2012 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Old_Recdef
     1.6  imports Wfrec
     1.7 -keywords "recdef" :: thy_decl
     1.8 +keywords "recdef" :: thy_decl and "permissive" "congs" "hints"
     1.9  uses
    1.10    ("~~/src/HOL/Tools/TFL/casesplit.ML")
    1.11    ("~~/src/HOL/Tools/TFL/utils.ML")
    1.12 @@ -42,7 +42,7 @@
    1.13  lemma tfl_eq_True: "(x = True) --> x"
    1.14    by blast
    1.15  
    1.16 -lemma tfl_rev_eq_mp: "(x = y) --> y --> x";
    1.17 +lemma tfl_rev_eq_mp: "(x = y) --> y --> x"
    1.18    by blast
    1.19  
    1.20  lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)"