theory hover
imports Main 
begin

definition mysucc::"nat => nat" where "mysucc n = n + 1" 

lemma "mysucc 1 = 2" by (simp add: mysucc_def)   

end