src/HOL/WF.ML
changeset 5278 a903b66822e2
parent 5148 74919e8f221c
child 5281 f4d16517b360
     1.1 --- a/src/HOL/WF.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -317,8 +317,7 @@
     1.4  
     1.5  (**** TFL variants ****)
     1.6  
     1.7 -Goal
     1.8 -    "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
     1.9 +Goal "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
    1.10  by (Clarify_tac 1);
    1.11  by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
    1.12  by (assume_tac 1);