This has been fixed. The new documentation and error message behaviour will be in the next release (expect it soon).
See https://github.com/mn200/HOL/issues/128 Thanks again, Michael On 10/08/13 23:45, Rob Arthan wrote: > I think the section on new_type_definition in the HOL 4 reference manual > should > say that it fails if the theorem in the parameter has free variables. E.g., > app load ["PairedLambda", "Q"]; open PairedLambda pairTheory; > val tyax1 = new_type_definition ("bad1", Q.prove(`?p.(\(x,y). ~(x /\ y /\ z)) > p`, > Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC [])); > correctly results in an error: > Exception- > HOL_ERR > {message = > "at Thm.prim_type_definition:\nsubset predicate must be a closed term", > origin_function = "new_type_definition", origin_structure = "Definition"} > raised > In fact, this is the only error message I can provoke: > val tyax2 = new_type_definition ("bad1", Q.prove(`?p.FST p \/ SND p`, > Q.EXISTS_TAC `(T,T)` THEN REWRITE_TAC [])); > results in the same exception even though what is wrong here is that the > theorem > doesn't have the form |= ?x.t x > Regards, > Rob. > ------------------------------------------------------------------------------ > Get 100% visibility into Java/.NET code with AppDynamics Lite! > It's a free troubleshooting tool designed for production. > Get down to code-level detail for bottlenecks, with <2% overhead. > Download for free and get started troubleshooting in minutes. > http://pubads.g.doubleclick.net/gampad/clk?id=48897031&iu=/4140/ostg.clktrk > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Introducing Performance Central, a new site from SourceForge and AppDynamics. Performance Central is your source for news, insights, analysis and resources for efficient Application Performance Management. Visit us today! http://pubads.g.doubleclick.net/gampad/clk?id=48897511&iu=/4140/ostg.clktrk
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
