src/HOL/IsaMakefile
changeset 41852 9aae2eed4696
parent 41827 98eda7ffde79
child 41854 b2b5b965b59c
equal deleted inserted replaced
41851:96184364aa6f 41852:9aae2eed4696
  1528 ## HOLCF-Library
  1528 ## HOLCF-Library
  1529 
  1529 
  1530 HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
  1530 HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
  1531 
  1531 
  1532 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
  1532 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
       
  1533   Library/Nat_Infinity.thy \
  1533   HOLCF/Library/Defl_Bifinite.thy \
  1534   HOLCF/Library/Defl_Bifinite.thy \
  1534   HOLCF/Library/Bool_Discrete.thy \
  1535   HOLCF/Library/Bool_Discrete.thy \
  1535   HOLCF/Library/Char_Discrete.thy \
  1536   HOLCF/Library/Char_Discrete.thy \
  1536   HOLCF/Library/HOL_Cpo.thy \
  1537   HOLCF/Library/HOL_Cpo.thy \
  1537   HOLCF/Library/Int_Discrete.thy \
  1538   HOLCF/Library/Int_Discrete.thy \
  1561 ## HOLCF-ex
  1562 ## HOLCF-ex
  1562 
  1563 
  1563 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
  1564 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
  1564 
  1565 
  1565 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
  1566 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
  1566   Library/Nat_Infinity.thy \
       
  1567   HOLCF/ex/Dagstuhl.thy \
  1567   HOLCF/ex/Dagstuhl.thy \
  1568   HOLCF/ex/Dnat.thy \
  1568   HOLCF/ex/Dnat.thy \
  1569   HOLCF/ex/Domain_Proofs.thy \
  1569   HOLCF/ex/Domain_Proofs.thy \
  1570   HOLCF/ex/Fix2.thy \
  1570   HOLCF/ex/Fix2.thy \
  1571   HOLCF/ex/Focus_ex.thy \
  1571   HOLCF/ex/Focus_ex.thy \