# HG changeset patch
# User nipkow
# Date 748194070 -7200
# Node ID 2695ba9b40f7fb85d888f7b88822c02e0b911bfb
# Parent  5f77582e3a89e72ec99dac10fe70743c0ba1d58e
added header

diff -r 5f77582e3a89 -r 2695ba9b40f7 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Sep 16 16:55:17 1993 +0200
+++ b/src/Provers/splitter.ML	Thu Sep 16 17:41:10 1993 +0200
@@ -1,5 +1,10 @@
-(*** case splitting ***)
-(*
+(*  Title:      Provers/splitter
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1993  TU Munich
+
+Generic case-splitter, suitable for most logics.
+
 Use:
 
 val split_tac = mk_case_split_tac iffD;
@@ -17,10 +22,7 @@
 val lift = prove_goal Pure.thy
   "[| !!x::'b::logic. Q(x) == R(x) |] ==> P(%x.Q(x)) == P(%x.R(x))::'a::logic"
   (fn [prem] => [rewtac prem, rtac reflexive_thm 1]);
-(*
-val iffD = prove_goal Pure.thy "[| PROP P == PROP Q; PROP Q |] ==> PROP P"
-  (fn [p1,p2] => [rtac (equal_elim (symmetric p1) p2) 1]);
-*)
+
 val trlift = lift RS transitive_thm;
 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;