src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16548 aa36ae6b955e
parent 16520 7a9cda53bfa2
child 16803 014090d1e64b
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jun 22 19:48:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jun 22 20:26:31 2005 +0200
     1.3 @@ -79,8 +79,8 @@
     1.4        "Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
     1.5  |   proofstep_to_string  (MRR ((a,b), (c,d))) =
     1.6        "MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
     1.7 -|   proofstep_to_string (Rewrite((a,b),(c,d))) =
     1.8 -      "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
     1.9 +(*|   proofstep_to_string (Rewrite((a,b),(c,d))) =
    1.10 +      "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
    1.11  
    1.12  fun list_to_string [] liststr = liststr
    1.13  |   list_to_string (x::[]) liststr = liststr^(string_of_int x)
    1.14 @@ -667,16 +667,16 @@
    1.15              >> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) =>  Factor (c,e,f))
    1.16  
    1.17  
    1.18 -val rewritestep = (a (Word "Rewrite"))  ++ (a (Other "(")) ++ (a (Other "(")) 
    1.19 +(*val rewritestep = (a (Word "Rewrite"))  ++ (a (Other "(")) ++ (a (Other "(")) 
    1.20                     ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
    1.21                     ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
    1.22 -            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))
    1.23 +            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))*)
    1.24  
    1.25  val obviousstep = (a (Word "Obvious")) ++ (a (Other "(")) 
    1.26                     ++ term_numstep  ++ (a (Other ")")) 
    1.27              >> (fn (_, (_, (c,_))) => Obvious (c))
    1.28  
    1.29 - val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || rewritestep || obviousstep
    1.30 + val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || (*rewritestep ||*) obviousstep
    1.31  
    1.32  
    1.33   val number_list_step =
    1.34 @@ -869,9 +869,9 @@
    1.35  |   by_isar_line ((Factor ((a,b,c)))) = 
    1.36      "by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
    1.37  		(string_of_int c)^" ])\n"
    1.38 -|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
    1.39 +(*|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
    1.40      "by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
    1.41 -		(string_of_int c)^" "^(string_of_int d)^" ])\n"
    1.42 +		(string_of_int c)^" "^(string_of_int d)^" ])\n"*)
    1.43  |   by_isar_line ( (Obvious ((a,b)))) =
    1.44      "by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
    1.45