src/HOL/IsaMakefile
changeset 23213 43553703267c
parent 23194 085fa3def13b
child 23243 a37d3e6e8323
equal deleted inserted replaced
23212:82881b1ae9c6 23213:43553703267c
   627 
   627 
   628 HOL-ex: HOL $(LOG)/HOL-ex.gz
   628 HOL-ex: HOL $(LOG)/HOL-ex.gz
   629 
   629 
   630 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
   630 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
   631   ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
   631   ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
   632   ex/BT.thy ex/BinEx.thy \
   632   ex/BT.thy ex/BinEx.thy ex/CTL.thy \
   633   ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \
   633   ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \
   634   ex/Eval_examples.thy ex/Random.thy \
   634   ex/Eval_examples.thy ex/Random.thy \
   635   ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
   635   ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
   636   ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
   636   ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
   637   ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
   637   ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \