# HG changeset patch
# User paulson
# Date 867054949 -7200
# Node ID fdb1768ebd3e2528e101a2317e7e889067cbfaae
# Parent  fbd4eb0cd0da0f46cc2c6ad8aa09c010ed4b61d9
New "congs" keyword for recdef theory section

diff -r fbd4eb0cd0da -r fdb1768ebd3e src/HOL/thy_syntax.ML
--- 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,