Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
changeset 55576 315dd5920114
parent 55575 a5e33e18fb5c
child 55772 367ec44763fd 
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 08:34:33 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Feb 19 08:34:34 2014 +0100
@@ -24,8 +24,8 @@
      get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
       (term * term list list) list list -> local_theory ->
       typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
-     rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term ->
-       term -> term -> term};
+     rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
+       term -> term -> term -> term};
 
   exception PRIMREC of string * term list;
 
@@ -95,8 +95,8 @@
    get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
     (term * term list list) list list -> local_theory ->
     typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
-   rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term ->
-     term -> term -> term};
+   rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
+     term -> term -> term -> term};
 
 structure Data = Theory_Data
 (
isabelle