# HG changeset patch
# User paulson
# Date 831138005 -7200
# Node ID eaecc8be539b51fcfc995573f8fe7b2f60150f42
# Parent  8d46452739d7b76574665ac06065ca53989f8aeb
updated comments for handling derivations

diff -r 8d46452739d7 -r eaecc8be539b src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Fri May 03 17:35:13 1996 +0200
+++ b/src/HOL/ex/mesontest.ML	Fri May 03 17:40:05 1996 +0200
@@ -6,9 +6,9 @@
 Test data for the MESON proof procedure
    (Excludes the equality problems 51, 52, 56, 58)
 
-show_hyps:=false;
+show_hyps := false;
 
-full_deriv:=false;
+keep_derivs := MinDeriv;
 by (rtac ccontr 1);
 val [prem] = gethyps 1;
 val nnf = make_nnf prem;
@@ -21,7 +21,7 @@
 
 goal HOL.thy "False";
 by (resolve_tac goes 1);
-full_deriv:=true;
+keep_derivs := FullDeriv;
 
 by (prolog_step_tac horns 1);
 by (iter_deepen_prolog_tac horns);