equal
deleted
inserted
replaced
|
1 (* Title: TFL/thms |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 *) |
|
6 |
1 structure Thms : Thms_sig = |
7 structure Thms : Thms_sig = |
2 struct |
8 struct |
3 val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec" |
9 val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec" |
4 val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct" |
10 val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct" |
5 val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply" |
11 val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply" |