A slight simplification of optstring
authorpaulson
Thu Jun 05 13:22:25 1997 +0200 (1997-06-05)
changeset 34036cc663f6d62e
parent 3402 9477a6410fe1
child 3404 91a91790899a
A slight simplification of optstring
The new "simpset" keyword in the "recdef" declaration
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Jun 05 13:21:41 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Jun 05 13:22:25 1997 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4           )
     1.5        end
     1.6      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
     1.7 -    fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
     1.8 +    fun optstring s = optional (s $$-- string >> trim) "[]"
     1.9    in
    1.10      repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
    1.11        >> mk_params
    1.12 @@ -231,7 +231,7 @@
    1.13  
    1.14  
    1.15  (*fname: name of function being defined; rel: well-founded relation*)
    1.16 -fun mk_rec_decl ((fname, rel), axms) =
    1.17 +fun mk_rec_decl (((fname, rel), ss), axms) =
    1.18    let val fid = trim fname
    1.19        val intrnl_name = fid ^ "_Intrnl"
    1.20    in
    1.21 @@ -246,13 +246,15 @@
    1.22            \  struct\n\
    1.23            \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
    1.24            \  val {rules, induct, tcs} = \n\
    1.25 -          \    \t Tfl.simplify_defn(thy, (" ^ quote fid ^ 
    1.26 +          \    \t Tfl.simplify_defn (" ^ ss ^ ") (thy, (" ^ quote fid ^ 
    1.27  					  ", pats_" ^ intrnl_name ^ "))\n\
    1.28            \  end;\n\
    1.29            \val pats_" ^ intrnl_name ^ " = ();\n")
    1.30    end;
    1.31  
    1.32 -val rec_decl = (name -- string -- repeat1 string >> mk_rec_decl) ;
    1.33 +val rec_decl = (name -- string -- 
    1.34 +		optional ("simpset" $$-- string >> trim) "!simpset" -- 
    1.35 +		repeat1 string >> mk_rec_decl) ;
    1.36  
    1.37  
    1.38  
    1.39 @@ -260,7 +262,7 @@
    1.40  
    1.41  (** sections **)
    1.42  
    1.43 -val user_keywords = ["intrs", "monos", "con_defs", "|"];
    1.44 +val user_keywords = ["intrs", "monos", "con_defs", "simpset", "|"];
    1.45  
    1.46  val user_sections =
    1.47   [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,