src/HOL/Library/BNF_Axiomatization.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 62691 9bfcbab7cd99
child 69605 a96320074298
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56942
5fff4dc31d34 bnf_decl -> bnf_axiomatization
traytel
parents: 55076
diff changeset
     1
(*  Title:      HOL/Library/BNF_Axiomatization.thy
54601
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
     3
    Copyright   2013
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
     4
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
     5
Axiomatic declaration of bounded natural functors.
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
     6
*)
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
     7
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59794
diff changeset
     8
section \<open>Axiomatic Declaration of Bounded Natural Functors\<close>
54601
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
     9
56942
5fff4dc31d34 bnf_decl -> bnf_axiomatization
traytel
parents: 55076
diff changeset
    10
theory BNF_Axiomatization
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 54601
diff changeset
    11
imports Main
54601
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
    12
keywords
56942
5fff4dc31d34 bnf_decl -> bnf_axiomatization
traytel
parents: 55076
diff changeset
    13
  "bnf_axiomatization" :: thy_decl
54601
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
    14
begin
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
    15
62691
9bfcbab7cd99 put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
blanchet
parents: 60500
diff changeset
    16
ML_file "../Tools/BNF/bnf_axiomatization.ML"
54601
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
    17
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff changeset
    18
end