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/ 
11:11 

silver joined #isabelle 
21:37 

chindy joined #isabelle 
21:41 
chindy 
is there some way to give an alias to an argument of a function like for example a function "function ((a,b) as p) = (if a then p else (b,a))" :: bool*bool => bool*bool 
22:22 
inte 
I don't think so, and it may even be impossible, because the function specification is parsed as term... so what would the meaning of "x as y" be if used as a term? ... too late. 