equal
deleted
inserted
replaced
186 |
186 |
187 (** primrec **) |
187 (** primrec **) |
188 |
188 |
189 fun mk_primrec_decl (alt_name, (names, eqns)) = |
189 fun mk_primrec_decl (alt_name, (names, eqns)) = |
190 ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^ |
190 ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^ |
191 ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^ |
191 ") = PrimrecPackage.add_primrec (" ^ alt_name ^ ") " ^ |
192 brackets (commas_quote names) ^ " " ^ brackets (commas eqns) ^ " thy;\n\ |
192 brackets (commas_quote names) ^ " " ^ brackets (commas eqns) ^ " thy;\n\ |
193 \val thy = thy\n"; |
193 \val thy = thy\n"; |
194 |
194 |
195 (* either names and axioms or just axioms *) |
195 (* either names and axioms or just axioms *) |
196 val primrec_decl = (optional ("(" $$-- name --$$ ")" >> (cat "Some")) "None" -- |
196 val primrec_decl = (optional ("(" $$-- name --$$ ")" >> (cat "Some")) "None" -- |