equal
deleted
inserted
replaced
1997 |
1997 |
1998 in fn (ctxt, t) => |
1998 in fn (ctxt, t) => |
1999 let |
1999 let |
2000 val vs = Term.add_frees t []; |
2000 val vs = Term.add_frees t []; |
2001 val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t; |
2001 val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t; |
2002 in (Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
2002 in (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
2003 end; |
2003 end; |
2004 *} |
2004 *} |
2005 |
2005 |
2006 ML_file "ferrack_tac.ML" |
2006 ML_file "ferrack_tac.ML" |
2007 |
2007 |