| changeset 45605 | a89b4bc311a5 |
| parent 44375 | dfc2e722fe47 |
| child 55017 | 2df6ad1dbd66 |
--- a/src/HOL/NanoJava/TypeRel.thy Sun Nov 20 20:59:30 2011 +0100 +++ b/src/HOL/NanoJava/TypeRel.thy Sun Nov 20 21:05:23 2011 +0100 @@ -86,7 +86,7 @@ apply auto done -lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard] +lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI] lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)" by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)