Time 
Nick 
Message 
02:48 

ilbot3 joined #isabelle 
02:48 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
08:55 

eng500 joined #isabelle 
09:30 

safinaskar joined #isabelle 
10:40 

safinaskar joined #isabelle 
11:45 
safinaskar 
what means that isabelle has 3 levels of lambda calculus? 
11:45 
safinaskar 
i see 2 only: one normal typed lambda calculus with (%x. ...) as lambda constructor and with "=>" for constructing function types. and another is logic itself with { assume "..." then have "..." by ... } as lambda constructor and "==>" for constructing "function types" (throught typecheckingproving isomorphism) 
11:45 
safinaskar 
where is 3rd? 
12:08 

eng500 joined #isabelle 
17:38 

safinaskar joined #isabelle 
18:49 

safinaskar joined #isabelle 
20:01 

safinaskar joined #isabelle 
20:08 

safinaskar left #isabelle 