--- a/src/HOL/thy_syntax.ML Fri Jun 20 13:19:31 1997 +0200
+++ b/src/HOL/thy_syntax.ML Mon Jun 23 10:35:49 1997 +0200
@@ -231,7 +231,7 @@
(*fname: name of function being defined; rel: well-founded relation*)
-fun mk_rec_decl (((fname, rel), ss), axms) =
+fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
let val fid = trim fname
val intrnl_name = fid ^ "_Intrnl"
in
@@ -246,13 +246,14 @@
\ struct\n\
\ val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
\ val {rules, induct, tcs} = \n\
- \ \t Tfl.simplify_defn (" ^ ss ^ ") (thy, (" ^ quote fid ^
- ", pats_" ^ intrnl_name ^ "))\n\
+ \ \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
+ \ \t\t (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
\ end;\n\
\val pats_" ^ intrnl_name ^ " = ();\n")
end;
val rec_decl = (name -- string --
+ optional ("congs" $$-- string >> trim) "[]" --
optional ("simpset" $$-- string >> trim) "!simpset" --
repeat1 string >> mk_rec_decl) ;
@@ -262,7 +263,7 @@
(** sections **)
-val user_keywords = ["intrs", "monos", "con_defs", "simpset", "|"];
+val user_keywords = ["intrs", "monos", "con_defs", "congs", "simpset", "|"];
val user_sections =
[axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,