Time 
Nick 
Message 
00:32 

aindilis joined #isabelle 
00:52 
Warrigal_ 
Yo. 
00:52 
Warrigal_ 
So Isabelle/Pure is the base system, right? Everything starts from there? 
00:55 
Warrigal_ 
I'd like to jump right in and start writing Isabelle/Pure, skipping Isabelle/HOL... but it's not obvious how I can learn how Isabelle/Pure works. 
00:55 
Warrigal_ 
I found something that pointed me at this, and it looks like it may be a good example to imitate: https://github.com/seL4/isabelle/blob/master/src/HOL/Isar_Examples/Higher_Order_Logic.thy 
00:55 
Warrigal_ 
But I haven't been able to find information about, say, what "class" means. 
01:26 

Warrigal_ joined #isabelle 
01:30 
Warrigal_ 
Can I... pretty much just declare whatever inference rules I want? 
01:36 
Warrigal_ 
What I'd like to say, perhaps, is that there's a thing called "flimcat", and that "flimcat" has the type "fp flimcat"... except it looks like maybe the head of a parameterized type is written on the right, in which case the type would be "flimcat fp". 
01:36 
Warrigal_ 
I'm not sure if you can declare something as having a type and then later declare it as additionally having a different type. 
01:38 
Warrigal_ 
Or whether each term must have exactly one type, no more and no less. 
01:50 
Warrigal_ 
Whelp, I guess I'll take another look at things later... 
01:51 

ilbot3 joined #isabelle 
01:51 

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/ 
03:29 
JCaesar 
qertyyyy: A lot of proofs seem to do 'finally show ?thesis ..' or 'finally show thesis .' depending on what you want, those might be your friends. (.. is equal to 'by rule', iirc, so it will apply refl if available. '.' is just by assumption, or so…) 
05:29 

ilbot3 joined #isabelle 
05:29 

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/ 
14:42 

ilbot3 joined #isabelle 
14:42 

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/ 
14:48 

ilbot3 joined #isabelle 
14: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/ 
15:16 

juanbono joined #isabelle 
21:29 

Warrigal_ joined #isabelle 
21:43 

Warriga_l joined #isabelle 
23:47 

Warrigal_ joined #isabelle 