New "congs" keyword for recdef theory section
authorpaulson
Mon Jun 23 10:35:49 1997 +0200 (1997-06-23)
changeset 3456fdb1768ebd3e
parent 3455 fbd4eb0cd0da
child 3457 a8ab7c64817c
New "congs" keyword for recdef theory section
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Jun 20 13:19:31 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon Jun 23 10:35:49 1997 +0200
     1.3 @@ -231,7 +231,7 @@
     1.4  
     1.5  
     1.6  (*fname: name of function being defined; rel: well-founded relation*)
     1.7 -fun mk_rec_decl (((fname, rel), ss), axms) =
     1.8 +fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
     1.9    let val fid = trim fname
    1.10        val intrnl_name = fid ^ "_Intrnl"
    1.11    in
    1.12 @@ -246,13 +246,14 @@
    1.13            \  struct\n\
    1.14            \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
    1.15            \  val {rules, induct, tcs} = \n\
    1.16 -          \    \t Tfl.simplify_defn (" ^ ss ^ ") (thy, (" ^ quote fid ^ 
    1.17 -					  ", pats_" ^ intrnl_name ^ "))\n\
    1.18 +          \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
    1.19 +          \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
    1.20            \  end;\n\
    1.21            \val pats_" ^ intrnl_name ^ " = ();\n")
    1.22    end;
    1.23  
    1.24  val rec_decl = (name -- string -- 
    1.25 +		optional ("congs" $$-- string >> trim) "[]" -- 
    1.26  		optional ("simpset" $$-- string >> trim) "!simpset" -- 
    1.27  		repeat1 string >> mk_rec_decl) ;
    1.28  
    1.29 @@ -262,7 +263,7 @@
    1.30  
    1.31  (** sections **)
    1.32  
    1.33 -val user_keywords = ["intrs", "monos", "con_defs", "simpset", "|"];
    1.34 +val user_keywords = ["intrs", "monos", "con_defs", "congs", "simpset", "|"];
    1.35  
    1.36  val user_sections =
    1.37   [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,