Added Keywords: "otherwise" and "sequential", needed for function package's
authorkrauss
Fri Aug 04 18:01:45 2006 +0200 (2006-08-04)
changeset 20338ecdfc96cf4d0
parent 20337 36e2fae2c68a
child 20339 d001121600ac
Added Keywords: "otherwise" and "sequential", needed for function package's
sequential mode.
etc/isar-keywords.el
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/pattern_split.ML
     1.1 --- a/etc/isar-keywords.el	Fri Aug 04 12:01:31 2006 +0200
     1.2 +++ b/etc/isar-keywords.el	Fri Aug 04 18:01:45 2006 +0200
     1.3 @@ -259,6 +259,7 @@
     1.4      "notes"
     1.5      "obtains"
     1.6      "open"
     1.7 +    "otherwise"
     1.8      "output"
     1.9      "outputs"
    1.10      "overloaded"
    1.11 @@ -267,6 +268,7 @@
    1.12      "pre"
    1.13      "rename"
    1.14      "restrict"
    1.15 +    "sequential"
    1.16      "shows"
    1.17      "signature"
    1.18      "states"
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Aug 04 12:01:31 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Aug 04 18:01:45 2006 +0200
     2.3 @@ -85,11 +85,6 @@
     2.4        val spec = map prep_eqns eqns_attss
     2.5        val t_eqnss = map (flat o map snd) spec
     2.6  
     2.7 -(*
     2.8 - val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns
     2.9 -              else t_eqns
    2.10 -*)
    2.11 -
    2.12        val congs = get_fundef_congs (Context.Theory thy)
    2.13  
    2.14        val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
    2.15 @@ -218,16 +213,16 @@
    2.16  
    2.17  val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
    2.18  
    2.19 -fun opt_thm_name_star s =
    2.20 -  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ s) ("", ([], false));
    2.21 +val opt_thm_name_star =
    2.22 +  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false));
    2.23  
    2.24  
    2.25  val function_decl =
    2.26 -    Scan.repeat1 (opt_thm_name_star ":" -- P.prop);
    2.27 +    Scan.repeat1 (opt_thm_name_star -- P.prop);
    2.28  
    2.29  val functionP =
    2.30    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    2.31 -  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "pre" -- P.$$$ ")") >> K true) false) --    
    2.32 +  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --    
    2.33    P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
    2.34                                      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
    2.35  
    2.36 @@ -237,6 +232,8 @@
    2.37         >> (fn (name,dom) =>
    2.38  	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
    2.39  
    2.40 +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
    2.41 +
    2.42  val _ = OuterSyntax.add_parsers [functionP];
    2.43  val _ = OuterSyntax.add_parsers [terminationP];
    2.44  
     3.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Fri Aug 04 12:01:31 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Fri Aug 04 18:01:45 2006 +0200
     3.3 @@ -103,14 +103,13 @@
     3.4  end
     3.5  
     3.6  
     3.7 -
     3.8  fun split_some_equations ctx eqns =
     3.9      let
    3.10 -      fun split_aux prevs [] = []
    3.11 +      fun split_aux prev [] = []
    3.12          | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
    3.13                                                            :: split_aux (eq :: prev) es
    3.14          | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq]) 
    3.15 -                                                                :: split_aux (eq :: prev) es
    3.16 +                                                           :: split_aux (eq :: prev) es
    3.17      in
    3.18        split_aux [] eqns
    3.19      end