equal
deleted
inserted
replaced
381 \verb! fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\ |
381 \verb! fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\ |
382 \verb! | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\ |
382 \verb! | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\ |
383 \verb! | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\ |
383 \verb! | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\ |
384 \verb! | my_lhs ctxt (_ $ t $ _) = t!\\ |
384 \verb! | my_lhs ctxt (_ $ t $ _) = t!\\ |
385 \verb! | my_lhs ctxt _ = error ("Binary operator expected")!\\ |
385 \verb! | my_lhs ctxt _ = error ("Binary operator expected")!\\ |
386 \verb! in [TermStyle.update_style "new_lhs" my_lhs]!\\ |
386 \verb! in [TermStyle.add_style "new_lhs" my_lhs]!\\ |
387 \verb!end;!\\ |
387 \verb!end;!\\ |
388 \verb!*!\verb!}!\\ |
388 \verb!*!\verb!}!\\ |
389 \end{quote} |
389 \end{quote} |
390 |
390 |
391 This example indeed shows a way the \verb!lhs! style could be implemented; |
391 This example indeed shows a way the \verb!lhs! style could be implemented; |