src/HOL/Tools/recdef_package.ML
author nipkow
Wed, 26 Jul 2000 19:42:19 +0200
changeset 9447 e5180c869772
parent 8734 b456aba346a6
child 9640 8c6cf4f01644
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/recdef_package.ML
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     4
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     5
Wrapper module for Konrad Slind's TFL package.
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     6
*)
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     7
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     8
signature RECDEF_PACKAGE =
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
     9
sig
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    10
  val quiet_mode: bool ref
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    11
  val print_recdefs: theory -> unit
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    12
  val get_recdef: theory -> string
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    13
    -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    14
  val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    15
    -> simpset option -> (xstring * Args.src list) list -> theory
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    16
    -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    17
  val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    18
    -> simpset option -> (thm * theory attribute list) list
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    19
    -> theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    20
  val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    21
    -> theory -> theory * {induct_rules: thm}
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    22
  val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    23
    -> theory -> theory * {induct_rules: thm}
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    24
  val setup: (theory -> theory) list
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    25
end;
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    26
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    27
structure RecdefPackage: RECDEF_PACKAGE =
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    28
struct
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    29
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    30
val quiet_mode = Tfl.quiet_mode;
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    31
val message = Tfl.message;
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    32
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    33
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    34
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    35
(** theory data **)
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    36
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    37
(* data kind 'HOL/recdef' *)
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    38
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    39
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    40
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    41
structure RecdefArgs =
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    42
struct
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    43
  val name = "HOL/recdef";
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    44
  type T = recdef_info Symtab.table;
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    45
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    46
  val empty = Symtab.empty;
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    47
  val copy = I;
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    48
  val prep_ext = I;
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    49
  val merge: T * T -> T = Symtab.merge (K true);
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    50
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    51
  fun print sg tab =
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    52
    Pretty.writeln (Pretty.strs ("recdefs:" ::
6851
526c0b90bcef cond_extern_table;
wenzelm
parents: 6729
diff changeset
    53
      map #1 (Sign.cond_extern_table sg Sign.constK tab)));
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    54
end;
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    55
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    56
structure RecdefData = TheoryDataFun(RecdefArgs);
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    57
val print_recdefs = RecdefData.print;
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    58
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    59
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    60
(* get and put data *)
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    61
8481
89d498a8d3f6 get_recdef now returns None instead of raising ERROR.
berghofe
parents: 8430
diff changeset
    62
fun get_recdef thy name = Symtab.lookup (RecdefData.get thy, name);
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    63
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    64
fun put_recdef name info thy =
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    65
  let
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    66
    val tab = Symtab.update_new ((name, info), RecdefData.get thy)
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    67
      handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    68
  in RecdefData.put tab thy end;
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    69
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    70
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    71
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    72
(** add_recdef(_i) **)
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    73
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    74
fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    75
8711
00ec2ba9174d outer syntax: no simps;
wenzelm
parents: 8657
diff changeset
    76
fun gen_add_recdef tfl_fn prep_att app_thms raw_name R eq_srcs opt_ss raw_congs thy =
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    77
  let
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    78
    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    79
    val bname = Sign.base_name name;
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    80
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
    81
    val _ = requires_recdef thy;
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    82
    val _ = message ("Defining recursive function " ^ quote name ^ " ...");
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
    83
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    84
    val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    85
    val eq_atts = map (map (prep_att thy)) raw_eq_atts;
8711
00ec2ba9174d outer syntax: no simps;
wenzelm
parents: 8657
diff changeset
    86
    val ss = if_none opt_ss (Simplifier.simpset_of thy);
7798
42e94b618f34 return stored thms with proper naming in derivation;
wenzelm
parents: 7262
diff changeset
    87
    val (thy, congs) = thy |> app_thms raw_congs;
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    88
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    89
    val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    90
    val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    91
    val simp_att = if null tcs then [Simplifier.simp_add_global] else [];
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    92
8430
dbd897e0d804 adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7798
diff changeset
    93
    val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    94
    val (thy, (simps' :: rules', [induct'])) =
7798
42e94b618f34 return stored thms with proper naming in derivation;
wenzelm
parents: 7262
diff changeset
    95
      thy
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
    96
      |> Theory.add_path bname
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    97
      |> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
8430
dbd897e0d804 adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7798
diff changeset
    98
      |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
    99
    val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
7798
42e94b618f34 return stored thms with proper naming in derivation;
wenzelm
parents: 7262
diff changeset
   100
    val thy =
42e94b618f34 return stored thms with proper naming in derivation;
wenzelm
parents: 7262
diff changeset
   101
      thy
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   102
      |> put_recdef name result
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   103
      |> Theory.parent_path;
7798
42e94b618f34 return stored thms with proper naming in derivation;
wenzelm
parents: 7262
diff changeset
   104
  in (thy, result) end;
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   105
8711
00ec2ba9174d outer syntax: no simps;
wenzelm
parents: 8657
diff changeset
   106
val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
00ec2ba9174d outer syntax: no simps;
wenzelm
parents: 8657
diff changeset
   107
val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
00ec2ba9174d outer syntax: no simps;
wenzelm
parents: 8657
diff changeset
   108
val add_recdef_i = gen_add_recdef Tfl.define_i (K I) IsarThy.apply_theorems_i;
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   109
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   110
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   111
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   112
(** defer_recdef(_i) **)
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   113
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   114
fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   115
  let
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   116
    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   117
    val bname = Sign.base_name name;
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   118
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   119
    val _ = requires_recdef thy;
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   120
    val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   121
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   122
    val (thy1, congs) = thy |> app_thms raw_congs;
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   123
    val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
8430
dbd897e0d804 adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7798
diff changeset
   124
    val (thy3, [induct_rules']) =
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   125
      thy2
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   126
      |> Theory.add_path bname
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   127
      |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
8430
dbd897e0d804 adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7798
diff changeset
   128
      |>> Theory.parent_path;
dbd897e0d804 adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7798
diff changeset
   129
  in (thy3, {induct_rules = induct_rules'}) end;
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   130
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   131
val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   132
val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   133
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   134
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   135
6439
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   136
(** package setup **)
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   137
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   138
(* setup theory *)
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   139
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   140
val setup = [RecdefData.init];
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   141
7eea9f25dc49 'HOL/recdef' theory data;
wenzelm
parents: 6429
diff changeset
   142
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   143
(* outer syntax *)
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   144
6723
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6576
diff changeset
   145
local structure P = OuterParse and K = OuterSyntax.Keyword in
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   146
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   147
val recdef_decl =
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
   148
  P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
8711
00ec2ba9174d outer syntax: no simps;
wenzelm
parents: 8657
diff changeset
   149
  Scan.optional (P.$$$ "congs" |-- P.!!! P.xthms1) []
00ec2ba9174d outer syntax: no simps;
wenzelm
parents: 8657
diff changeset
   150
  >> (fn (((f, R), eqs), congs) => #1 o add_recdef_x f R (map P.triple_swap eqs) None congs);
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   151
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   152
val recdefP =
6723
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6576
diff changeset
   153
  OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   154
    (recdef_decl >> Toplevel.theory);
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   155
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   156
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   157
val defer_recdef_decl =
8657
b9475dad85ed recdef: admit names/atts;
wenzelm
parents: 8625
diff changeset
   158
  P.name -- Scan.repeat1 P.prop --
6723
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6576
diff changeset
   159
  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   160
  >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   161
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   162
val defer_recdefP =
6723
f342449d73ca outer syntax keyword classification;
wenzelm
parents: 6576
diff changeset
   163
  OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   164
    (defer_recdef_decl >> Toplevel.theory);
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   165
8734
b456aba346a6 removed obsolete "simpset" keyword;
wenzelm
parents: 8711
diff changeset
   166
val _ = OuterSyntax.add_keywords ["congs"];
6557
d7e7532c128a peoper defer_recdef interface;
wenzelm
parents: 6520
diff changeset
   167
val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
6429
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   168
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   169
end;
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   170
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   171
9771ce553e56 Wrapper module for Konrad Slind's TFL package.
wenzelm
parents:
diff changeset
   172
end;