src/HOL/BNF/BNF_Def.thy
changeset 51836 4d6dcd51dd52
parent 49537 fe1deee434b6
child 51893 596baae88a88
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Tue Apr 30 13:23:52 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Tue Apr 30 13:34:31 2013 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  imports BNF_Util
     1.5  keywords
     1.6    "print_bnfs" :: diag and
     1.7 -  "bnf_def" :: thy_goal
     1.8 +  "bnf" :: thy_goal
     1.9  begin
    1.10  
    1.11  lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"