src/HOL/Codatatype/Codatatype.thy
author blanchet
Tue, 11 Sep 2012 17:14:49 +0200
changeset 49283 97809ae5f7bb
parent 49123 263b0e330d8b
child 49286 dde4967c9233
permissions -rw-r--r--
move "bnf_util.ML" to "BNF_Util.thy"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Codatatype/Codatatype.thy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
49017
66fc7fc2d49b started work on datatype sugar
blanchet
parents: 48975
diff changeset
     3
    Author:     Andrei Popescu, TU Muenchen
66fc7fc2d49b started work on datatype sugar
blanchet
parents: 48975
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
The (co)datatype package.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     9
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
header {* The (Co)datatype Package *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    12
theory Codatatype
49283
97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy"
blanchet
parents: 49123
diff changeset
    13
imports BNF_LFP BNF_GFP BNF_Wrap
49112
4de4635d8f93 started work on sugared "(co)data" commands
blanchet
parents: 49075
diff changeset
    14
keywords
4de4635d8f93 started work on sugared "(co)data" commands
blanchet
parents: 49075
diff changeset
    15
  "data" :: thy_decl
4de4635d8f93 started work on sugared "(co)data" commands
blanchet
parents: 49075
diff changeset
    16
and
4de4635d8f93 started work on sugared "(co)data" commands
blanchet
parents: 49075
diff changeset
    17
  "codata" :: thy_decl
4de4635d8f93 started work on sugared "(co)data" commands
blanchet
parents: 49075
diff changeset
    18
uses
49123
263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents: 49112
diff changeset
    19
  "Tools/bnf_fp_sugar_tactics.ML"
49112
4de4635d8f93 started work on sugared "(co)data" commands
blanchet
parents: 49075
diff changeset
    20
  "Tools/bnf_fp_sugar.ML"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    21
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    22
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    23
end