{"action":"created","issue":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/251","labels_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/251/labels{/name}","comments_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/251/comments","events_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/251/events","html_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/251","id":65924253,"number":251,"title":"Trial","user":{"login":"jeremydaw","id":9719896,"avatar_url":"https://avatars.githubusercontent.com/u/9719896?v=3","gravatar_id":"","url":"https://api.github.com/users/jeremydaw","html_url":"https://github.com/jeremydaw","followers_url":"https://api.github.com/users/jeremydaw/followers","following_url":"https://api.github.com/users/jeremydaw/following{/other_user}","gists_url":"https://api.github.com/users/jeremydaw/gists{/gist_id}","starred_url":"https://api.github.com/users/jeremydaw/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jeremydaw/subscriptions","organizations_url":"https://api.github.com/users/jeremydaw/orgs","repos_url":"https://api.github.com/users/jeremydaw/repos","events_url":"https://api.github.com/users/jeremydaw/events{/privacy}","received_events_url":"https://api.github.com/users/jeremydaw/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-04-02T13:27:11Z","updated_at":"2015-04-29T06:40:24Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/pulls/251","html_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/251","diff_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/251.diff","patch_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/251.patch"},"body":"tactic RULE_L_ASSUM_TAC, like RULE_ASSUM_TAC but f produces list of theorems\r\n\r\nexample -  RULE_L_ASSUM_TAC CONJUNCTS  splits all conjuncts in assumptions of goal"},"comment":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/comments/97323909","html_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/251#issuecomment-97323909","issue_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/251","id":97323909,"user":{"login":"mn200","id":145647,"avatar_url":"https://avatars.githubusercontent.com/u/145647?v=3","gravatar_id":"","url":"https://api.github.com/users/mn200","html_url":"https://github.com/mn200","followers_url":"https://api.github.com/users/mn200/followers","following_url":"https://api.github.com/users/mn200/following{/other_user}","gists_url":"https://api.github.com/users/mn200/gists{/gist_id}","starred_url":"https://api.github.com/users/mn200/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mn200/subscriptions","organizations_url":"https://api.github.com/users/mn200/orgs","repos_url":"https://api.github.com/users/mn200/repos","events_url":"https://api.github.com/users/mn200/events{/privacy}","received_events_url":"https://api.github.com/users/mn200/received_events","type":"User","site_admin":false},"created_at":"2015-04-29T06:40:24Z","updated_at":"2015-04-29T06:40:24Z","body":"Also, in the updated proofs in `containerTheory`, there are a few places where you have excessive parentheses.  For example\r\n\r\n    EVERY [(tac1), (tacfn arg), (foo bar baz)]\r\n\r\nis unnecessary and could be \r\n\r\n    EVERY [tac1, tacfn arg, foo bar baz]\r\n\r\nLikewise, a few places where you have parentheses in `THEN` chains (though these can sometimes be necessary, as *per* FAQ)."}}