src/HOL/Transitive_Closure.thy
changeset 15096 be1d3b8cfbd5
parent 15076 4b3d280ef06a
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Aug 02 09:44:46 2004 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Aug 02 10:12:02 2004 +0200
     1.3 @@ -462,19 +462,7 @@
     1.4      val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
     1.5      val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
     1.6      val rtrancl_trans = thm "rtrancl_trans";
     1.7 -(*
     1.8 -  fun decomp (Trueprop $ t) = 
     1.9 -    let fun dec (Const ("op :", _) $ t1 $ t2 ) = 
    1.10 -	let fun dec1  (Const ("Pair", _) $ a $ b) =  (a,b);
    1.11 -	    fun dec2 (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    1.12 -	      | dec2 (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    1.13 -	      | dec2 r = (r,"r");
    1.14 -	    val (a,b) = dec1 t1;
    1.15 -	    val (rel,r) = dec2 t2;
    1.16 -	in Some (a,b,rel,r) end
    1.17 -      | dec _ =  None 
    1.18 -    in dec t end;
    1.19 -*)
    1.20 +
    1.21    fun decomp (Trueprop $ t) = 
    1.22      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = 
    1.23  	let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")