Added coherent logic prover.
authorberghofe
Mon Sep 22 23:04:35 2008 +0200 (2008-09-22)
changeset 283274d7a0a941b79
parent 28326 ddd53738dae8
child 28328 9a647179c1e6
Added coherent logic prover.
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 22 23:01:54 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 22 23:04:35 2008 +0200
     1.3 @@ -153,6 +153,7 @@
     1.4    $(SRC)/Provers/blast.ML \
     1.5    $(SRC)/Provers/clasimp.ML \
     1.6    $(SRC)/Provers/classical.ML \
     1.7 +  $(SRC)/Provers/coherent.ML \
     1.8    $(SRC)/Provers/eqsubst.ML \
     1.9    $(SRC)/Provers/hypsubst.ML \
    1.10    $(SRC)/Provers/order.ML \
    1.11 @@ -763,7 +764,7 @@
    1.12    Library/Primes.thy							\
    1.13    ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy	\
    1.14    ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
    1.15 -  ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy			\
    1.16 +  ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
    1.17    ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
    1.18    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
    1.19    ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\