# HG changeset patch
# User paulson
# Date 880711242 -3600
# Node ID 2335f6584a1b562df8dbbfe3c0b59027e8b794e4
# Parent  7211ea5f29e2c1989ed658169cdf4bba2dc3bdd0
Added comments

diff -r 7211ea5f29e2 -r 2335f6584a1b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Nov 28 10:59:14 1997 +0100
+++ b/src/HOL/simpdata.ML	Fri Nov 28 11:00:42 1997 +0100
@@ -396,11 +396,14 @@
   (fn _ => [rtac ext 1, rtac refl 1]);
 
 
+(*For expand_case_tac*)
 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
 by (case_tac "P" 1);
 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
 val expand_case = result();
 
+(*Used in Auth proofs.  Typically P contains Vars that become instantiated
+  during unification.*)
 fun expand_case_tac P i =
     res_inst_tac [("P",P)] expand_case i THEN
     Simp_tac (i+1) THEN