# HG changeset patch
# User paulson
# Date 855912942 -3600
# Node ID cc4eb23d37b30b39fcbe1a963c06830020f82f25
# Parent  28232396b60eab506cf40657977c52e44be818c4
Updated documentation of IFOL_ss

diff -r 28232396b60e -r cc4eb23d37b3 doc-src/Ref/simplifier.tex
--- 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 = 
   empty_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];