isabelle: src/HOLCF/ax_ops/thy_syntax.ML@85898be702b2 (annotated)

1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	1	(* Title: HOLCF/thy_syntax.ML
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	2	ID: $Id$
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	3	Author: Tobias Mayr
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	4
3618 1e7621573d9c obsolete! wenzelm parents: 3609 diff changeset	5	Additional thy file sections for HOLCF: axioms, ops.
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7
3622 85898be702b2 use ThySyn.add_syntax; wenzelm parents: 3618 diff changeset	8	ThySyn.add_syntax
85898be702b2 use ThySyn.add_syntax; wenzelm parents: 3618 diff changeset	9	(ThyAxioms.axioms_keywords @ ThyOps.ops_keywords)
85898be702b2 use ThySyn.add_syntax; wenzelm parents: 3618 diff changeset	10	(ThyAxioms.axioms_sections @ ThyOps.ops_sections);