| changeset 23850 | f1434532a562 |
| parent 23250 | 9886802cbbd6 |
| child 24193 | 926dde4d96de |
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Jul 19 15:37:37 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Thu Jul 19 21:47:34 2007 +0200 @@ -1,6 +1,3 @@ -structure ROOT = -struct - structure HOL = struct @@ -26,5 +23,3 @@ HOL.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2; end; (*struct Codegen*) - -end; (*struct ROOT*)