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