Updated documentation of IFOL_ss
Fri, 14 Feb 1997 10:35:42 +0100
changeset 2613 cc4eb23d37b3
parent 2612 28232396b60e
child 2614 0b1364481214
Updated documentation of IFOL_ss
--- a/doc-src/Ref/simplifier.tex	Fri Feb 14 10:35:23 1997 +0100
+++ b/doc-src/Ref/simplifier.tex	Fri Feb 14 10:35:42 1997 +0100
@@ -937,7 +937,8 @@
 The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}.
 It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt
   mk_meta_eq}.  It solves simplified subgoals using {\tt triv_rls} and
-assumptions.  It uses \ttindex{asm_simp_tac} to tackle subgoals of
+assumptions, and by detecting contradictions.  
+It uses \ttindex{asm_simp_tac} to tackle subgoals of
 conditional rewrites.  It takes {\tt IFOL_rews} as rewrite rules.  
 Other simpsets built from {\tt IFOL_ss} will inherit these items.
 In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite
@@ -948,8 +949,9 @@
 val IFOL_ss = 
   setmksimps (map mk_meta_eq o atomize o gen_all)
-  setsolver  (fn prems => resolve_tac (triv_rls \at prems) ORELSE' 
-                          assume_tac)
+  setsolver  (fn prems => resolve_tac (triv_rls \at prems)
+                          ORELSE' assume_tac
+                          ORELSE' etac FalseE)
   setsubgoaler asm_simp_tac
   addsimps IFOL_rews
   addcongs [imp_cong];