equal
deleted
inserted
replaced
1 (* Title: ZF/Datatype_ZF.thy |
1 (* Title: ZF/Datatype_ZF.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1997 University of Cambridge |
3 Copyright 1997 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section{*Datatype and CoDatatype Definitions*} |
6 section\<open>Datatype and CoDatatype Definitions\<close> |
7 |
7 |
8 theory Datatype_ZF |
8 theory Datatype_ZF |
9 imports Inductive_ZF Univ QUniv |
9 imports Inductive_ZF Univ QUniv |
10 keywords "datatype" "codatatype" :: thy_decl |
10 keywords "datatype" "codatatype" :: thy_decl |
11 begin |
11 begin |
12 |
12 |
13 ML_file "Tools/datatype_package.ML" |
13 ML_file "Tools/datatype_package.ML" |
14 |
14 |
15 ML {* |
15 ML \<open> |
16 (*Typechecking rules for most datatypes involving univ*) |
16 (*Typechecking rules for most datatypes involving univ*) |
17 structure Data_Arg = |
17 structure Data_Arg = |
18 struct |
18 struct |
19 val intrs = |
19 val intrs = |
20 [@{thm SigmaI}, @{thm InlI}, @{thm InrI}, |
20 [@{thm SigmaI}, @{thm InlI}, @{thm InrI}, |
105 |
105 |
106 |
106 |
107 val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc; |
107 val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc; |
108 |
108 |
109 end; |
109 end; |
110 *} |
110 \<close> |
111 |
111 |
112 setup {* |
112 setup \<open> |
113 Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv]) |
113 Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv]) |
114 *} |
114 \<close> |
115 |
115 |
116 end |
116 end |