author | nipkow |
Mon, 13 Mar 1995 09:42:50 +0100 | |
changeset 950 | 323f8ca4587a |
parent 949 | 83c588d6fee9 |
child 951 | 682139612060 |
src/HOL/WF.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/WF.ML Mon Mar 13 09:38:10 1995 +0100 +++ b/src/HOL/WF.ML Mon Mar 13 09:42:50 1995 +0100 @@ -8,8 +8,7 @@ open WF; -val H_cong = read_instantiate [("f","H::[?'a, ?'a=>?'b]=>?'b")] - (standard(refl RS cong RS cong)); +val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); val H_cong1 = refl RS H_cong; (*Restriction to domain A. If r is well-founded over A then wf(r)*)