src/FOL/IsaMakefile
changeset 44121 44adaa6db327
parent 42799 4e33894aec6d
child 45860 93eda35a8377
equal deleted inserted replaced
44120:01de796250a0 44121:44adaa6db327
    27 
    27 
    28 $(OUT)/Pure: Pure
    28 $(OUT)/Pure: Pure
    29 
    29 
    30 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
    30 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
    31   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    31   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    32   $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML	\
    32   $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML		\
    33   $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML	\
    33   $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
       
    34   $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
    34   $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
    35   $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
    35   $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
    36   $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
    36   $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
    37   $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
    37   $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    38   $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    38   $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
    39   $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\