On 17/09/13 00:13, Makarius wrote: > When you have an Isar command, its main functionality needs to be > available directly in ML as well. That is an automatism, without > thinking. For the opposite you would have to provide a proof over > future uses of your tool. > > There is a certain standard naming scheme and implementation scheme to > provide both some foobar and foobar_cmd simultaneously. To reiterate my question, does that mean you want a "Fun_Cases.fun_cases" command that takes a term and a string and registers the fun_cases rule derived from the term under the given name?
> It does, you merely need to look further. (It also takes time, so I > would rather give up the feature here). > > Note that Proof_Context.read_pattern is for reading patterns, as the > name says. This gives you quite different policies for type checking, > and lots of potential for surprise. From where did you get the idea > to use Proof_Context.read_pattern? It is hardly ever used in existing > sources at all. I honestly don't remember. With the documentation on Isabelle/ML being so sparse, one is, as a beginner, all but forced to experiment with snippets of code from other parts of Isabelle until stuff works, and that's what I did. At any rate, I suppose I can simply remove the dummy pattern feature again. Cheers, Manuel _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
