-
Notifications
You must be signed in to change notification settings - Fork 2
/
pure_isaplib.thy
61 lines (49 loc) · 1.77 KB
/
pure_isaplib.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
theory pure_isaplib
imports Pure
begin
(* basic logging, testing and project tools. *)
ML_file "basics/log.ML"
(* names *)
ML_file "names/namer.ML"
ML_file "names/namers.ML" (* instances of namer, StrName, etc *)
ML_file "names/basic_nameset.ML" (* basic sets of names *)
ML_file "names/basic_nametab.ML" (* name tables which provide fresh names *)
ML_file "names/basic_renaming.ML" (* renaming, based on tables and sets *)
(* generic Name structure; provies nametables, namesets and collections *)
ML_file "names/basic_name.ML"
ML_file "names/compound_renaming.ML" (* renaming within datatypes *)
ML_file "names/renaming.ML" (* renamings which can be renamed *)
(* as above, but with renaming *)
ML_file "names/nameset.ML"
ML_file "names/nametab.ML"
(* names + renaming for them, their tables, sets, and renamings *)
ML_file "names/names.ML"
(* Binary Relations of finite name sets: good for dependencies *)
ML_file "names/name_map.ML" (* functions/mappings on names *)
ML_file "names/name_inj.ML" (* name iso-morphisms *)
ML_file "names/name_injendo.ML" (* name auto-morphisms (name iso where dom = cod) *)
ML_file "names/name_binrel.ML" (* bin relations on names *)
ML_file "names/names_common.ML"
(* unif stuff *)
ML_file "unif/unif_data.ML"
ML_file "unif/umorph.ML"
(* graphs *)
ML_file "graph/pregraph.ML"
ML_file "graph/rgraph.ML"
(* maps *)
ML_file "maps/abstract_map.ML"
ML_file "maps/name_table.ML"
ML_file "maps/name_relation.ML"
ML_file "maps/name_function.ML"
ML_file "maps/name_injection.ML"
ML_file "maps/name_substitution.ML"
(* search *)
ML_file "search/gsearch.ML"
ML_file "search/msearch.ML"
ML_file "search/lsearch.ML"
(* Other basic top level things *)
ML_file "basics/collection.ML"
ML_file "basics/polym_table.ML"
ML_file "basics/text_socket.ML"
ML_file "basics/toplevel.ML"
end