src/HOL/Codatatype/BNF_Def.thy
author blanchet
Tue Sep 11 17:09:39 2012 +0200 (2012-09-11)
changeset 49282 c057e1b39f16
parent 48975 7f79f94a432c
child 49283 97809ae5f7bb
permissions -rw-r--r--
renamed "BNF_Library" to "BNF_Util"
blanchet@48975
     1
(*  Title:      HOL/Codatatype/BNF_Def.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Definition of bounded natural functors.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Definition of Bounded Natural Functors *}
blanchet@48975
     9
blanchet@48975
    10
theory BNF_Def
blanchet@49282
    11
imports BNF_Util
blanchet@48975
    12
keywords
blanchet@48975
    13
  "print_bnfs" :: diag
blanchet@48975
    14
and
blanchet@48975
    15
  "bnf_def" :: thy_goal
blanchet@48975
    16
uses
blanchet@48975
    17
  "Tools/bnf_util.ML"
blanchet@48975
    18
  "Tools/bnf_tactics.ML"
blanchet@48975
    19
  "Tools/bnf_def.ML"
blanchet@48975
    20
begin
blanchet@48975
    21
blanchet@48975
    22
end