Re: [isabelle] how to know which rules to apply before apply(auto)?



Becoming an expert at Isabelle takes time and cannot be rushed. It sounds like you simply need to work through the tutorials, doing small examples to begin with. Before attempting to prove a theorem, you need to have an intuitive grasp of the key steps of the proof. Don’t expect “auto” to work miracles. 

Larry Paulson


> On 26 Oct 2014, at 09:11, M A <tesleft at hotmail.com> wrote:
> 
> Hi
> 1. how to know which rules to apply before apply(auto)?2. any manual to show all the rules that can be applied for each library when import them?3. is there any difference to apply rules in one statement or apply one by one?
> a. apply(a)apply(b)done
> b.apply(a,b)done
> 
> Regards,
> Martin 		 	   		  





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