equal
deleted
inserted
replaced
150 |
150 |
151 (** dataype theorems **) |
151 (** dataype theorems **) |
152 |
152 |
153 structure TheoremsData = TheoryDataFun |
153 structure TheoremsData = TheoryDataFun |
154 (struct |
154 (struct |
155 val name = "Pure/theorems"; |
|
156 type T = |
155 type T = |
157 {theorems: thm list NameSpace.table, |
156 {theorems: thm list NameSpace.table, |
158 index: FactIndex.T} ref; |
157 index: FactIndex.T} ref; |
159 |
158 |
160 fun mk_empty _ = |
159 fun mk_empty _ = |
503 val A = Free ("A", propT); |
502 val A = Free ("A", propT); |
504 |
503 |
505 val proto_pure = |
504 val proto_pure = |
506 Context.pre_pure_thy |
505 Context.pre_pure_thy |
507 |> Compress.init_data |
506 |> Compress.init_data |
508 |> Sign.init_data |
|
509 |> Theory.init_data |
|
510 |> Proofterm.init_data |
|
511 |> TheoremsData.init |
507 |> TheoremsData.init |
512 |> Sign.add_types |
508 |> Sign.add_types |
513 [("fun", 2, NoSyn), |
509 [("fun", 2, NoSyn), |
514 ("prop", 0, NoSyn), |
510 ("prop", 0, NoSyn), |
515 ("itself", 1, NoSyn), |
511 ("itself", 1, NoSyn), |