* support sub/super scripts (for single symbols only), input syntax is
like this: "A\<^sup>*" or "A\<^sup>\<star>";
* antiquotation @{goals} for output of *dynamic* goals state; Note
that presentation of goal states does not conform to actual
human-readable proof documents. Please do not include goal states
into document output unless you really know what you are doing!
(* Title: TFL/thms.sml
ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
*)
signature Thms_sig =
sig
val WF_INDUCTION_THM: thm
val WFREC_COROLLARY: thm
val CUT_DEF: thm
val SELECT_AX: thm
val eqT: thm
val rev_eq_mp: thm
val simp_thm: thm
end;
structure Thms: Thms_sig =
struct
val WFREC_COROLLARY = get_thm Wellfounded_Recursion.thy "tfl_wfrec";
val WF_INDUCTION_THM = get_thm Wellfounded_Recursion.thy "tfl_wf_induct";
val CUT_DEF = get_thm Wellfounded_Recursion.thy "cut_def";
val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
(fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
val eqT = prove"(x = True) --> x";
val rev_eq_mp = prove"(x = y) --> y --> x";
val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)";
end;