Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added datatype_case.ML and nominal_fresh_fun.ML.
authorberghofe
Tue, 24 Apr 2007 15:19:33 +0200
changeset 22784 4637b69de71b
parent 22783 e5f947e0ade8
child 22785 fab155c8ce46
Added datatype_case.ML and nominal_fresh_fun.ML.
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/IsaMakefile	Tue Apr 24 15:18:42 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 24 15:19:33 2007 +0200
@@ -98,7 +98,7 @@
   Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy		\
   Sum_Type.thy Tools/res_reconstruct.ML Tools/ATP/reduce_axiomsN.ML	\
   Tools/ATP/watcher.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML		\
-  Tools/datatype_aux.ML Tools/datatype_codegen.ML				\
+  Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML	\
   Tools/datatype_hooks.ML Tools/datatype_package.ML				\
   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML		\
@@ -730,6 +730,7 @@
 $(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
   Nominal/Nominal.thy \
   Nominal/nominal_atoms.ML \
+  Nominal/nominal_fresh_fun.ML \
   Nominal/nominal_induct.ML \
   Nominal/nominal_inductive.ML \
   Nominal/nominal_package.ML \
isabelle