Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_function_core.ML
changeset 2848 da7e6655cd4c
parent 2822 23befefc6e73
child 2862 47063163f333 
--- a/Nominal/nominal_function_core.ML	Tue Jun 14 11:43:06 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jun 14 14:07:07 2011 +0100
@@ -290,6 +290,7 @@
     val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
 
     val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
+
   in if j < i then
     let
       val compat = lookup_compat_thm j i cts
nominal2