src/ZF/thy_syntax.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 3399 0c4efa9eac29
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     1
(*  Title:      ZF/thy_syntax.ML
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     2
    ID:         $Id$
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     5
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     6
Additional theory file sections for ZF
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     7
*)
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     8
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     9
structure ThySynData: THY_SYN_DATA =
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    10
struct
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    11
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    12
(*Inductive definitions theory section.   co is either "" or "Co"*)
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    13
fun inductive_decl co =
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    14
  let open ThyParse 
1428
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    15
    fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    16
        if Syntax.is_identifier s then "op " ^ s  else "_"
1428
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    17
    fun mk_params ((((((rec_tms, sdom_sum), ipairs), 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    18
                      monos), con_defs), type_intrs), type_elims) =
1428
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    19
      let val big_rec_name = space_implode "_" 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    20
                           (map (scan_to_id o trim) rec_tms)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    21
          and srec_tms = mk_list rec_tms
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    22
          and sintrs   = mk_big_list (map snd ipairs)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    23
          val stri_name = big_rec_name ^ "_Intrnl"
1428
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    24
      in
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    25
         (";\n\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    26
          \structure " ^ stri_name ^ " =\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    27
          \  struct\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    28
          \  val _ = writeln \"" ^ co ^ 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    29
                     "Inductive definition " ^ big_rec_name ^ "\"\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    30
          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) "
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    31
                           ^ srec_tms ^ "\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    32
          \  and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    33
          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    34
                           ^ sintrs ^ "\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    35
          \  end;\n\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    36
          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    37
             stri_name ^ ".rec_tms, " ^
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    38
             stri_name ^ ".dom_sum, " ^
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    39
             stri_name ^ ".intr_tms)"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    40
         ,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    41
          "structure " ^ big_rec_name ^ " =\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    42
          \ let\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    43
          \  val _ = writeln \"Proofs for " ^ co ^ 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    44
                     "Inductive definition " ^ big_rec_name ^ "\"\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    45
          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    46
          \\t  (open " ^ stri_name ^ "\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    47
          \\t   val thy\t\t= thy\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    48
          \\t   val monos\t\t= " ^ monos ^ "\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    49
          \\t   val con_defs\t\t= " ^ con_defs ^ "\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    50
          \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    51
          \\t   val type_elims\t= " ^ type_elims ^ ")\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    52
          \ in\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    53
          \  struct\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    54
          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    55
          \  open Result\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    56
          \  end\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    57
          \ end;\n\n\
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    58
          \structure " ^ stri_name ^ " = struct end;\n\n"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    59
         )
1428
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    60
      end
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    61
    val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    62
    val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    63
    fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    64
  in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    65
             -- optstring "type_intrs" -- optstring "type_elims"
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    66
     >> mk_params
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    67
  end;
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    68
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    69
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    70
(*Datatype definitions theory section.   co is either "" or "Co"*)
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    71
fun datatype_decl co =
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    72
  let open ThyParse 
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    73
      (*generate strings*)
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    74
      fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    75
      val mk_data = mk_list o map mk_const o snd
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    76
      val mk_scons = mk_big_list o map mk_data
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    77
      fun mk_intr_name s =  (*the "op" cancels any infix status*)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    78
          if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    79
      fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    80
        let val rec_names = map (scan_to_id o trim o fst) rec_pairs
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    81
            val big_rec_name = space_implode "_" rec_names
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    82
            and srec_tms = mk_list (map fst rec_pairs)
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    83
            and scons    = mk_scons rec_pairs
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    84
            and sdom_sum = 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    85
                if dom = "" then  (*default domain: univ or quniv*)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    86
                    "Ind_Syntax." ^ co ^ "data_domain rec_tms"
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    87
                else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    88
            val stri_name = big_rec_name ^ "_Intrnl"
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    89
            val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    90
        in
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    91
           (";\n\n\
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    92
            \structure " ^ stri_name ^ " =\n\
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    93
            \  struct\n\
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    94
            \  val _ = writeln \"" ^ co ^ 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    95
                       "Datatype definition " ^ big_rec_name ^ "\"\n\
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
    96
            \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    97
            \  val dom_sum\t= " ^ sdom_sum ^ "\n\
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
    98
            \  and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n" 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    99
                   ^ scons ^ "\n\
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   100
            \  val intr_tms\t= Ind_Syntax.mk_all_intr_tms (rec_tms, con_ty_lists)\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   101
            \  end;\n\n\
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   102
            \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   103
                 mk_list (map quote rec_names) ^ ", " ^ 
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   104
                 stri_name ^ ".con_ty_lists) \n\
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   105
            \              |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   106
               stri_name ^ ".rec_tms, " ^
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   107
               stri_name ^ ".dom_sum, " ^
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   108
               stri_name ^ ".intr_tms)"
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   109
           ,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   110
            "structure " ^ big_rec_name ^ " =\n\
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   111
            \ let\n\
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   112
            \  val _ = writeln \"Proofs for " ^ co ^ 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   113
                       "Datatype definition " ^ big_rec_name ^ "\"\n\
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   114
            \  structure Result = " ^ co ^ "Data_section_Fun\n\
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   115
            \\t  (open " ^ stri_name ^ "\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   116
            \\t   val thy\t\t= thy\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   117
            \\t   val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   118
            \\t   val monos\t\t= " ^ monos ^ "\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   119
            \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   120
            \\t   val type_elims\t= " ^ type_elims ^ ");\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   121
            \ in\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   122
            \  struct\n\
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   123
            \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   124
            \  open Result\n\
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   125
            \  end\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   126
            \ end;\n\n\
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 797
diff changeset
   127
            \structure " ^ stri_name ^ " = struct end;\n\n"
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   128
           )
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   129
        end
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   130
      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   131
      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   132
      val construct = name -- string_list -- opt_mixfix;
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   133
  in optional ("<=" $$-- string) "" --
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   134
     enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   135
     optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   136
     >> mk_params
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   137
end;
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   138
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   139
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   140
(** Section specifications **)
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   141
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   142
val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   143
                     "and", "|", "<=", "domains", "intrs", "monos", 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   144
                     "con_defs", "type_intrs", "type_elims"];
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   145
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   146
val user_sections = [("inductive",  inductive_decl ""),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   147
                     ("coinductive",  inductive_decl "Co"),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   148
                     ("datatype",  datatype_decl ""),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
   149
                     ("codatatype",  datatype_decl "Co")];
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   150
end;
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   151
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   152
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   153
structure ThySyn = ThySynFun(ThySynData);
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   154
init_thy_reader ();