blob: 33ccd62718677e8e3735ac66787b091b911a9e0a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(*Generated by Lem from pervasives_extra.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory lem_function_extraTheory lem_maybe_extraTheory lem_map_extraTheory lem_num_extraTheory lem_set_extraTheory lem_set_helpersTheory lem_list_extraTheory lem_string_extraTheory lem_assert_extraTheory lem_show_extraTheory lem_machine_wordTheory;
val _ = numLib.prefer_num();
val _ = new_theory "lem_pervasives_extra"
(*include import Pervasives*)
(*include import Function_extra Maybe_extra Map_extra Num_extra Set_extra Set_helpers List_extra String_extra Assert_extra Show_extra Machine_word*)
val _ = export_theory()
|
