equal
deleted
inserted
replaced
140 |
140 |
141 $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) |
141 $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) |
142 @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base |
142 @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base |
143 |
143 |
144 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\ |
144 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\ |
|
145 Big_Operators.thy \ |
145 Complete_Lattice.thy \ |
146 Complete_Lattice.thy \ |
146 Datatype.thy \ |
147 Datatype.thy \ |
147 Extraction.thy \ |
148 Extraction.thy \ |
148 Fields.thy \ |
149 Fields.thy \ |
149 Finite_Set.thy \ |
150 Finite_Set.thy \ |