[isabelle] How do Isabelle use logic table to prove exist some, all, belong to



Hi  Larry,
i use logic table  that can prove  And , Or,  Implication  quickly by  from more  one  to less  one.
But  can not  search  logic table for exist some, all, belong to, idempotent relation  these  higher order concepts  in books, wiki  or web.
1. how  do Isabelle do  with  these  concept  to prove  with  logic  table? or  solved by programming skill  together with  more one to less  one? how  do  it do?
2.  I want to research the subgoals between A and  B when prove A -> B after quick decide that it is true with table method, what  is the  name of  algorithms  used in Isabelle  to generate  subgoals?         is there  any books teaching  these  algorithms to generate  subgoals?
Regards,
Martin Lee 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.