Hi Bill, I'm pondering the issue of miz3 not allowing free variables in contrast with how you want to work in an axiomatic framework. However, already:
> !(===) (Between:point#point#point->bool) (cong). > TarskiModel((===),(Between:point#point#point->bool),(cong)) > let (===) be point#point->point#point->bool; > let (Between) be point#point#point->bool; > let (cong) be point#point#point->point#point#point->bool; > assume TarskiModel((===),(Between:point#point#point->bool),(cong)) [0]; The !... line can be avoided by using "now". "!x. A ==> B proof ... end;" can also be written as "now let x be ...; assume A; ...; thus B; end;". And then the "now" can be omitted if it's on the very outside. I think. Also, the assume line doesn't need the typings. It will be parsed in the context of the "let"s. So you can just write "assume TarskiModel((===),Between,cong);" or something in that style. But I agree: having these four lines at the start of every lemma is very unattractive. Freek ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
