changeset 35145 | f132a4fd8679 |
parent 35144 | 8b8302da3a55 |
child 35146 | f7bf73b0d7e5 |
--- a/src/HOL/Record.thy Tue Feb 16 13:35:42 2010 +0100 +++ b/src/HOL/Record.thy Tue Feb 16 14:08:39 2010 +0100 @@ -437,7 +437,6 @@ "_record" :: "fields => 'a" ("(3'(| _ |'))") "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") - "_update_name" :: idt "_update" :: "ident => 'a => update" ("(2_ :=/ _)") "" :: "update => updates" ("_") "_updates" :: "update => updates => updates" ("_,/ _")