src/HOL/thy_syntax.ML
author clasohm
Wed, 04 Oct 1995 13:10:03 +0100
changeset 1264 3eb91524b938
parent 1251 81fc4d8e3eda
child 1316 ce35d42d2190
permissions -rw-r--r--
added local simpsets; removed IOA from 'make test'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/thy_syntax.ML
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
Additional theory file sections for HOL.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
TODO:
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
  move datatype / primrec stuff to pre_datatype.ML (?)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
(*the kind of distinctiveness axioms depends on number of constructors*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
val dtK = 5;  (* FIXME rename?, move? *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
structure ThySynData: THY_SYN_DATA =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
struct
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
open ThyParse;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
(** subtype **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
  let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
    val name' = if_none opt_name t;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
    val name = strip_quotes name';
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
  in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
      [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
        "Abs_" ^ name ^ "_inverse"])
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
val subtype_decl =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
  optional ("(" $$-- name --$$ ")" >> Some) None --
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
  >> mk_subtype_decl;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
(** (co)inductive **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
(*co is either "" or "Co"*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
fun inductive_decl co =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
  let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
    fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
      if Syntax.is_identifier s then "op " ^ s else "_";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
    fun mk_params (((recs, ipairs), monos), con_defs) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
      let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
          and srec_tms = mk_list recs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
          and sintrs   = mk_big_list (map snd ipairs)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    50
          val stri_name = big_rec_name ^ "_Intrnl"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
      in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
         (";\n\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
          \structure " ^ stri_name ^ " =\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    54
          \ let open Ind_Syntax in\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
          \  struct\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
          \  val _ = writeln \"" ^ co ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
                     "Inductive definition " ^ big_rec_name ^ "\"\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
          \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
                           ^ srec_tms ^ "\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
                           ^ sintrs ^ "\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
          \  end\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
          \ end;\n\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
             stri_name ^ ".rec_tms, " ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
             stri_name ^ ".intr_tms)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    67
         ,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
          "structure " ^ big_rec_name ^ " =\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
          \  struct\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
          \  (open " ^ stri_name ^ "\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
          \   val thy\t\t= thy\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
          \   val monos\t\t= " ^ monos ^ "\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
          \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
          \  open Result\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
          \  end\n"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
         )
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
      end
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
    val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
    fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
  in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
    repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
      >> mk_params
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    88
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    89
(** datatype **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    90
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    91
local
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    92
  (* FIXME err -> add_datatype *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    93
  fun mk_cons cs =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    94
    (case duplicates (map (fst o fst) cs) of
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    95
      [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    96
    | dups => error ("Duplicate constructors: " ^ commas_quote dups));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    97
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    98
  (*generate names of distinctiveness axioms*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    99
  fun mk_distinct_rules cs tname =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   100
    let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   101
      val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   102
      (*combine all constructor names with all others w/o duplicates*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   103
      fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   104
      fun neg1 [] = []
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   105
        | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   106
    in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   107
      if length uqcs < dtK then neg1 uqcs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   108
      else quote (tname ^ "_ord_distinct") ::
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   109
        map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   110
    end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   111
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   112
  fun mk_rules tname cons pre = " map (get_axiom thy) " ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   113
    mk_list (map (fn ((s, _), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   114
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   115
  (*generate string for calling add_datatype*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   116
  fun mk_params ((ts, tname), cons) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   117
   ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   118
    ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   119
    \val thy = thy",
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   120
    "structure " ^ tname ^ " =\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   121
    \struct\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   122
    \ val inject = map (get_axiom thy) " ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   123
        mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   124
          (filter_out (null o snd o fst) cons)) ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   125
    \ val distinct = " ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   126
        (if length cons < dtK then "let val distinct' = " else "") ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   127
        "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   128
        (if length cons < dtK then
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   129
          "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   130
          \ distinct') end"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   131
         else "") ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   132
    \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   133
    \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   134
    \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   135
    \ val simps = inject @ distinct @ cases @ recs;\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   136
    \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   137
    \end;\n\
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   138
    \val dummy = Addsimps " ^ tname ^ ".simps;\n");
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   139
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   140
  (*parsers*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   141
  val tvars = type_args >> map (cat "dtVar");
1251
81fc4d8e3eda added nested types on right hand side of datatype definitions
clasohm
parents: 977
diff changeset
   142
  fun complex_typ toks =
81fc4d8e3eda added nested types on right hand side of datatype definitions
clasohm
parents: 977
diff changeset
   143
    (("(" $$-- complex_typ  --$$ ")" >> (fn x => [x]) || tvars)
81fc4d8e3eda added nested types on right hand side of datatype definitions
clasohm
parents: 977
diff changeset
   144
     -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list)
81fc4d8e3eda added nested types on right hand side of datatype definitions
clasohm
parents: 977
diff changeset
   145
     || type_var >> cat "dtVar") toks;
977
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 923
diff changeset
   146
  val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) ||
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 923
diff changeset
   147
    type_var >> cat "dtVar";
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 923
diff changeset
   148
  val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   149
  val constructor = name -- opt_typs -- opt_mixfix;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   150
in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   151
  val datatype_decl =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   152
    (* FIXME tvars -> type_args *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   153
    tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   154
end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   155
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   156
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   157
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   158
(** primrec **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   159
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   160
fun mk_primrec_decl ((fname, tname), axms) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   161
  let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   162
    fun mk_prove (name, eqn) =
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   163
      "val " ^ name ^ " = store_thm (" ^ quote name
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   164
      ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   165
      \  (fn _ => [Simp_tac 1]));";
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   166
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   167
    val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   168
  in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   169
      ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   170
  end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   171
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   172
val primrec_decl =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   173
  name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   174
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   175
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   176
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   177
(** sections **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   178
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   179
val user_keywords = ["intrs", "monos", "con_defs", "|"];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   180
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   181
val user_sections =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   182
 [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   183
  ("inductive", inductive_decl ""),
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   184
  ("coinductive", inductive_decl "Co"),
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   185
  ("datatype", datatype_decl),
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   186
  ("primrec", primrec_decl)];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   187
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   188
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   189
end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   190
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   191
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   192
structure ThySyn = ThySynFun(ThySynData);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   193
init_thy_reader ();
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   194