equal
deleted
inserted
replaced
115 |
115 |
116 $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) |
116 $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) |
117 @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base |
117 @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base |
118 |
118 |
119 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\ |
119 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\ |
|
120 Complete_Lattice.thy \ |
120 Datatype.thy \ |
121 Datatype.thy \ |
121 Divides.thy \ |
122 Divides.thy \ |
122 Extraction.thy \ |
123 Extraction.thy \ |
123 Finite_Set.thy \ |
124 Finite_Set.thy \ |
124 Fun.thy \ |
125 Fun.thy \ |