Time 
Nick 
Message 
06:16 

dmiles_afk joined #isabelle 
06:36 

dmiles_afk joined #isabelle 
08:01 

dmiles_afk joined #isabelle 
14:11 

safinaskari joined #isabelle 
14:14 
safinaskari 
how to do structural induction on type like 'datatype tree = node "tree list"'? logicsHOL.pdf says I should do induction using 'induct_tac "x1 x2" i', but how exactly to do this? please give me some example 
14:48 
safinaskari 
assume i have "datatype obj = nth_obj nat". how to prove "bij nth_obj"? 
14:49 
safinaskari 
maybe this is already proved? 
15:22 

safinaskari left #isabelle 
22:33 

ski joined #isabelle 
22:33 

leonweber1 joined #isabelle 
22:34 

dmiles_afk joined #isabelle 
22:36 

kini joined #isabelle 
22:36 

mal`` joined #isabelle 