forked from Isabelle_DOF/Isabelle_DOF
2c01a7118b
- Add a term antiquotation for document classes and add the term* command which mimics the classical term command and adds the possibility to use a term antiquotation which references document classes: one can use @{A ''A_instance''} to reference an instance of the class A in a term* command. - Reuse and update the ML_isa_check_generic visitor pattern to add the function which checks the class instance of a class, used by the term antiquotation for document classes. Also, the update_isa functions now expect long name (See builtin term antiquotations setup) - The merge of ISA_transformer_tab has been update to avoid conflicts. Indeed, the merge is ultra-critical: the transformer tabs were just extended by letting *the first* entry with the same long-name win. Since the range is a (call-back) function, a comparison on its content is impossible and some choice has to be made. An alternative may be to use Symtab.join - As classes names as constants are already bound to "doc_class Regular_Exp.rexp" constants by add_doc_class_cmd function, we use a prefix "doc_class_" when adding document classes term antiquotations |
||
---|---|---|
.. | ||
latex | ||
Assert.thy | ||
AssertLong.thy | ||
Isa_COL.thy | ||
Isa_DOF.thy | ||
RegExpInterface.thy |