Time 
Nick 
Message 
02:47 

ilbot3 joined #isabelle 
02:47 

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/ 
02:52 

ammbauer joined #isabelle 
12:14 

silver joined #isabelle 
16:36 
inte 
is there a trick to get natural numbers displayed as numbers in Isabelle's output (jedit, output panel...) when evaluating expressions? 
16:39 
inte 
Okay, this I can work with: converting to int helps. 
16:45 
larsrh 
inte: I'm unaware of anything better than that 
16:52 
ammbauer 
importing "~~/src/HOL/Library/Code_Target_Nat"? 
16:52 
ammbauer 
https://stackoverflow.com/questions/22687646/simplifyprettyprintingofnaturals 
16:52 
larsrh 
cool, TIL 
17:03 
inte 
ammbauer: thanks, I didn't expect that ... uhm ... side effect. 
17:52 
ThreeOfEight 
inte: I actually hacked something together for that a while ago 
17:53 
ThreeOfEight 
I was planning to put it into the distribution at some point 
17:55 
ThreeOfEight 
inte: http://downthetypehole.de/paste/geC6Ll0U 
17:55 
ThreeOfEight 
This works. 
17:55 
ThreeOfEight 
Of course, the computations are a bit slow because this uses unary numbers internally 
17:55 
ThreeOfEight 
but it's enough for small examples 
17:56 

silver joined #isabelle 
17:57 
ThreeOfEight 
this also changes the output for quickcheck 