# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1319996710 0 # Node ID 32323727af96a17ed7275dec3e972014ee7f007d # Parent ae49c5e8868eeedc53e7ba6d34ffd6f9d2c4bd9e# Parent 7a84649d88397bd15da5f0706ec5474abe33f84b updated diff -r 7a84649d8839 -r 32323727af96 ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Sat Oct 29 13:17:12 2011 +0100 +++ b/ProgTutorial/Advanced.thy Sun Oct 30 17:45:10 2011 +0000 @@ -187,7 +187,7 @@ The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as *} -ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*} +ML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*} text {* Morphisms can be composed with the function @{ML_ind "$>" in Morphism} diff -r 7a84649d8839 -r 32323727af96 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Sat Oct 29 13:17:12 2011 +0100 +++ b/ProgTutorial/Essential.thy Sun Oct 30 17:45:10 2011 +0000 @@ -2225,7 +2225,7 @@ *} ML{*structure MyThms = Named_Thms - (val name = "attr_thms" + (val name = @{binding "attr_thms"} val description = "Theorems for an Attribute") *} text {* diff -r 7a84649d8839 -r 32323727af96 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Sat Oct 29 13:17:12 2011 +0100 +++ b/ProgTutorial/First_Steps.thy Sun Oct 30 17:45:10 2011 +0000 @@ -1245,7 +1245,7 @@ *} ML{*structure FooRules = Named_Thms - (val name = "foo" + (val name = @{binding "foo"} val description = "Theorems for foo") *} text {* diff -r 7a84649d8839 -r 32323727af96 progtutorial.pdf Binary file progtutorial.pdf has changed