src/HOL/Tools/refute_isar.ML
author boehmes
Mon, 08 Nov 2010 12:13:44 +0100
changeset 40424 7550b2cba1cb
parent 39048 4006f5c3f421
permissions -rw-r--r--
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     1
(*  Title:      HOL/Tools/refute_isar.ML
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     2
    Author:     Tjark Weber
22092
ab3dfcef6489 reformatted to 80 chars/line
webertj
parents: 17273
diff changeset
     3
    Copyright   2003-2007
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     4
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     5
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     6
end;
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     7