equal
deleted
inserted
replaced
80 "_datatype_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
80 "_datatype_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
81 "_datatype_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900) |
81 "_datatype_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900) |
82 |
82 |
83 named_theorems datatype_record_update |
83 named_theorems datatype_record_update |
84 |
84 |
85 ML_file "datatype_records.ML" |
85 ML_file \<open>datatype_records.ML\<close> |
86 setup \<open>Datatype_Records.setup\<close> |
86 setup \<open>Datatype_Records.setup\<close> |
87 |
87 |
88 end |
88 end |