# HG changeset patch
# User paulson
# Date 926067028 -7200
# Node ID 2d47dee036b536ef34973777509f20749224bbc7
# Parent  250a0ca35ef549f7a47856fb876bf25bfd8d7bb0
tidied

diff -r 250a0ca35ef5 -r 2d47dee036b5 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Fri May 07 10:48:56 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML	Fri May 07 10:50:28 1999 +0200
@@ -9,8 +9,6 @@
 (*split_all_tac causes a big blow-up*)
 claset_ref() := claset() delSWrapper record_split_name;
 
-Delsimps [split_paired_All];
-
 Goal "[| x ~: A;  y : A |] ==> x ~= y";
 by (Blast_tac 1);
 qed "not_mem_distinct";
@@ -55,7 +53,7 @@
 
 
 val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
-(* [| Lprg : B LeadsTo C; Lprg : A LeadsTo B |] ==> Lprg : (A Un B) LeadsTo C *)
+(* [| Lprg: B LeadsTo C; Lprg: A LeadsTo B |] ==> Lprg: (A Un B) LeadsTo C *)
 
 
 (*Simplification for records*)