# isabelle_session_info

session_name: ZF
input_heaps: 52b3290b17664489a5025e5db07f657813f5ca7e Pure
output_heap: 493d4d4b61b28314e3fe15542c3d8652afdc61fe ZF
uuid: f4d0b8cc-3021-4020-803e-5b0721c1f50c
sources:
9e34dd4840771596cb3ac075834d912a2330d598 <meta_info>
df53c2db173bd3260823a6189daa0dc68dabd8d2 ~~/src/FOL/FOL.thy
060cc15757e3dcc535cb63d5d9e68918f05ab401 ~~/src/FOL/IFOL.thy
b473ba489a05579a5b6c2317f76def106bf3a137 ~~/src/FOL/fologic.ML
228ec6545c1e72150b0dfaa862505c5999b0f301 ~~/src/FOL/intprover.ML
814507ab0cbf5596aec62422cb97090009c38294 ~~/src/FOL/simpdata.ML
8b037afc55aed139c994553c45a02b42bc35cf4d ~~/src/Provers/Arith/cancel_numerals.ML
95691b390de96e59c43ada2d5c92acc4b7eb93a5 ~~/src/Provers/Arith/combine_numerals.ML
a030ac8026f3f3f807ea1db1c376e666a1f1323b ~~/src/Provers/blast.ML
faa0ebb2dbea444d5f75ec88d022d5908c88f6ce ~~/src/Provers/clasimp.ML
ca46a51e7bdd86df1ef9e23e9f33e3ffddebadde ~~/src/Provers/classical.ML
bb1d43e441c55288107b99f81949664cd22d08ce ~~/src/Provers/hypsubst.ML
07deb34c3328fc4beb2a212a442d411e10c2790f ~~/src/Provers/quantifier1.ML
6ceecc864a779e2c4ba3ca44d697c675fadb8faf ~~/src/Provers/splitter.ML
404a2e2aea12e071c5038f50737573f8e014bc8f ~~/src/Pure/Concurrent/cache.ML
00d476eeabf48c6a071351016d91117be0ff3f08 ~~/src/Pure/Concurrent/counter.ML
05aca44a9017f38984e3a8af339ea430c08fd679 ~~/src/Pure/Concurrent/event_timer.ML
c818a6c26df54381d5bb55694438e98572494a3a ~~/src/Pure/Concurrent/future.ML
4d1af0037063afaefd76f62750e58b8e9b703211 ~~/src/Pure/Concurrent/isabelle_thread.ML
1da47b8a5cec4b586fde4ba6f038dfc6cd41e0c7 ~~/src/Pure/Concurrent/lazy.ML
cd7ca55e617c91ba73100435d95368dc229c03a5 ~~/src/Pure/Concurrent/mailbox.ML
24d2e1691935ee6b6cc59fb494eb03101e962a89 ~~/src/Pure/Concurrent/multithreading.ML
3ee8232188b406c8e5a458094cd4051c75c31316 ~~/src/Pure/Concurrent/par_exn.ML
eb0ceb7cd138688ca681bb23f79640e69f9c3df7 ~~/src/Pure/Concurrent/par_list.ML
d2832fff6e082779a8c032dc59ad4a5952f676c6 ~~/src/Pure/Concurrent/single_assignment.ML
a690b216f0cd94c39271b039259349b28b9461c9 ~~/src/Pure/Concurrent/synchronized.ML
553f3ea7972c31f79511f102057c32fab9527f48 ~~/src/Pure/Concurrent/task_queue.ML
271c20fad419fc1033841024b55fab026a94fd13 ~~/src/Pure/Concurrent/thread_attributes.ML
26ea6acc8115d898619592a611789a329a244e01 ~~/src/Pure/Concurrent/thread_data.ML
b61d466ea09654b217162d941472bba0c0164b8c ~~/src/Pure/Concurrent/thread_data_virtual.ML
49689820adcb6798248a34e13b363b8817806277 ~~/src/Pure/Concurrent/thread_position.ML
5fea4dfd00a9d7d2e4aa6814391bf56eff076de4 ~~/src/Pure/Concurrent/timeout.ML
0bb7680a5094816f45680f271bff72e36ad9c6e7 ~~/src/Pure/Concurrent/unsynchronized.ML
59cc6e1764892d38bad2bdf9cd2cdbedb08196f6 ~~/src/Pure/General/alist.ML
bb8e641035ddaaa1c93ffbc94176f73d6de296a5 ~~/src/Pure/General/antiquote.ML
c5d98a19252c891aba2817e34fc34eec0ed99fb0 ~~/src/Pure/General/array.ML
4417d3d96cf1ae5b5bb7eb7ff7137cda07ef0658 ~~/src/Pure/General/balanced_tree.ML
1490286bb32125b996c226556d795f0f3dc9f7cd ~~/src/Pure/General/base64.ML
c34461d7804726b25e017fee748a074c7a073765 ~~/src/Pure/General/basics.ML
4a13b38b1fd3a7ea5a36feb078b6e7bcab9f8b55 ~~/src/Pure/General/binding.ML
b52db8ab95ceedcb839dee878a2989fe64fff9f5 ~~/src/Pure/General/buffer.ML
24fbe9d081d4928e3da9fd23d4d4986563dbf4b7 ~~/src/Pure/General/bytes.ML
9e04313152c3dc3e40e2eb22d72d946b7ba91c81 ~~/src/Pure/General/change_table.ML
666b47042b967c8af41c6e59867bb679047f4610 ~~/src/Pure/General/comment.ML
2e0dea577c14854df7c3829af00cf04116bad2c9 ~~/src/Pure/General/completion.ML
7449cecf941d22a87c3039ce1578683e307b7c48 ~~/src/Pure/General/exn.ML
d873ad7129959c55060a938b95f758d2c32bde13 ~~/src/Pure/General/file.ML
8133338085c81541429170b00724213d6f09ff45 ~~/src/Pure/General/file_stream.ML
1f0a5110c4321b63111817509d6569b11e5d9ac2 ~~/src/Pure/General/graph.ML
23709bd5cd0da52113cc5bd5ce23ef91b042e14d ~~/src/Pure/General/graph_display.ML
87089639971c23259bf3c66a36012aa3ce341705 ~~/src/Pure/General/heap.ML
bdf92005c750f599a6bd57d180832a096f86974c ~~/src/Pure/General/input.ML
2cf125660f483ffdbc6f87d1a0a99e8e8f38f403 ~~/src/Pure/General/integer.ML
17f7ee69d5a65d7ede44cd86db00486ddac1c79b ~~/src/Pure/General/linear_set.ML
aaa1ffaa2953d73c57b46319e4b253ed6040c430 ~~/src/Pure/General/long_name.ML
f01b61cee3e9343a0ed91f2320c09f015398aab9 ~~/src/Pure/General/name_space.ML
a9d79e74775e752ad01192ab385f530b6d59e8ed ~~/src/Pure/General/ord_list.ML
1fe800a62f385a605b9415a1ed8558fa19611875 ~~/src/Pure/General/output.ML
99f1448e1d4209d614eea443db1826dd05da6bf0 ~~/src/Pure/General/output_primitives.ML
a3b96443d529bd47c001da109866e7d0f31e159b ~~/src/Pure/General/output_primitives_virtual.ML
9bd280d1c8027d94d515e336114ef615ac726489 ~~/src/Pure/General/path.ML
b3032edbf3fe3796fc4e5969833b082d57fec9fb ~~/src/Pure/General/position.ML
b6443e1756788f5f066c94482da1b81b5c430aaa ~~/src/Pure/General/pretty.ML
bba40ae3bda781bb83febfb58b6a196a00085654 ~~/src/Pure/General/print_mode.ML
8f442da3e04e866f9fcdf2b39e59e12195b5d470 ~~/src/Pure/General/properties.ML
f79e29ab7e341f19cd5c93719ebb33700c0f0097 ~~/src/Pure/General/queue.ML
476933b41be47d63e423bae2fab262a7227207a2 ~~/src/Pure/General/random.ML
85c6a63882e1b3829586722d1bce37e3ad7be05f ~~/src/Pure/General/rat.ML
bf34e3f8867a9d155aa3c00fe82114c586a41768 ~~/src/Pure/General/same.ML
46517145b916bc8b9be99ea26b4f6dc59d9f5138 ~~/src/Pure/General/scan.ML
7cc07648b3915eb2d95efbeab6a7c06dd23c7cb7 ~~/src/Pure/General/seq.ML
6b4572894438b81d84641d6199e248833e3e1757 ~~/src/Pure/General/set.ML
d0a47cd0f4d4f06391d17f51b2d64d5150256bd4 ~~/src/Pure/General/sha1.ML
6f8668a3c5386e317df48f9d82ffdb51b47af433 ~~/src/Pure/General/socket_io.ML
bd69dada09c85804688ceb66c8bf01f5f3396fb2 ~~/src/Pure/General/source.ML
a225475fb6ee5ce9420a1961385d073f754cd813 ~~/src/Pure/General/stack.ML
9bcbde1d4f0c968de6a06cf1c059fe6edfa16911 ~~/src/Pure/General/string.ML
64c5ee0d80ec3b12a7dc7c413da45430ab65b258 ~~/src/Pure/General/symbol.ML
cc8b2f26a7ea03208b428fa345c9ae540b2ba982 ~~/src/Pure/General/symbol_explode.ML
cdd38b923bd0faf04f48fa3c9a2e79782be4a62f ~~/src/Pure/General/symbol_pos.ML
5f0f223400fd2e6bf72f80ff92e0ca95c7229a72 ~~/src/Pure/General/table.ML
77e6a9800b665622936c5f0ad276bc04ebfaadf3 ~~/src/Pure/General/time.ML
b25fbc63f27d0651d28589c10b4dcb5eba983760 ~~/src/Pure/General/timing.ML
f1aa4aaddf76bdbc05e76a6cd5d70178884167a4 ~~/src/Pure/General/url.ML
d25c6d60ede692639fc1bc359ef7cee611caa341 ~~/src/Pure/General/utf8.ML
04b4a1dc03b556832d39f6dff5b512d6ccfc3f93 ~~/src/Pure/General/value.ML
aa57a4c48944b94333753eb785df9788ac64d55a ~~/src/Pure/General/vector.ML
fe7c9fb886a702dfdf4c31b62ddbd421a1018106 ~~/src/Pure/General/xz.ML
347b43aee4dd6d1cf15c5f5139446f89e4f48bda ~~/src/Pure/General/zstd.ML
99d1dedb9a97615e1b461b0eb41a2d6d29c81a7b ~~/src/Pure/Isar/args.ML
831c93dfb81c1feb8b4e2462ed17f752981ab709 ~~/src/Pure/Isar/attrib.ML
cb9728d15363a3fbcf61331908a8eb3b4bfcc979 ~~/src/Pure/Isar/auto_bind.ML
cebb275a22e1f6479fe5a5abfe1c27044b7cc93b ~~/src/Pure/Isar/bundle.ML
ba80614821d1fcaa2a6ff87c30825eb444116a1e ~~/src/Pure/Isar/calculation.ML
2806606a9f7911c7105d11005e668d096bfd3572 ~~/src/Pure/Isar/class.ML
135fb2eb5f81c183e5781bd1d6cc4dcebe5fe5fc ~~/src/Pure/Isar/class_declaration.ML
b1bc7850c29a301263d5226ff5e5e409a58225c3 ~~/src/Pure/Isar/code.ML
9979a4c1aca7a6d0906c6a37ebc0a8ca1bb06bbd ~~/src/Pure/Isar/context_rules.ML
33f8c701ce0ee30f5af90f4c2affadd63c142dd8 ~~/src/Pure/Isar/element.ML
c3642d2d069fffacfa16f5911055e28290faa45d ~~/src/Pure/Isar/entity.ML
b2c795961ca9502b5e1129093f2abbe28665a439 ~~/src/Pure/Isar/experiment.ML
ea3cdb166f7a588ed8f326346db71e6b8825da54 ~~/src/Pure/Isar/expression.ML
bbf5afad62895236de5a8ba810fc3fcc4637a912 ~~/src/Pure/Isar/generic_target.ML
57ded5ddbeae2c75efdaf83aedd32246e203f68f ~~/src/Pure/Isar/interpretation.ML
8237df0f04075b1bf8787321154e188e019e6e9c ~~/src/Pure/Isar/isar_cmd.ML
2ab296838234b2b09219a3cb617fb8862c50ae4c ~~/src/Pure/Isar/keyword.ML
ad0a3cbe51b1e2a534652ac9650a1435c6ac1a1d ~~/src/Pure/Isar/local_defs.ML
ec84e827c93b2dcde6a76c199065e5a7ef2b510e ~~/src/Pure/Isar/local_theory.ML
80cef8d221652c30230aaa2ccc69935f7a620703 ~~/src/Pure/Isar/locale.ML
1e14a6a719fc84af24c4923a59260a871e5bb7dc ~~/src/Pure/Isar/method.ML
34330278962468b89d8bca5af0a8c2356e45f9c4 ~~/src/Pure/Isar/named_target.ML
4ef7e8bd81a67af2954f3b45043341fe68fa3f8a ~~/src/Pure/Isar/object_logic.ML
aa547461658e8be086b9d7ab235bcb25fe41b810 ~~/src/Pure/Isar/obtain.ML
f1b3405794a3d8e2a60efe793a109afeefd48bf2 ~~/src/Pure/Isar/outer_syntax.ML
a3b07cdc20bd7ac7f53d712f91f17d295bd88499 ~~/src/Pure/Isar/overloading.ML
dda1a11f7bd3e01b29cb3b5954f9076a853ab8ec ~~/src/Pure/Isar/parse.ML
033288f97ea40ba8650970958dbd317d8810a4e9 ~~/src/Pure/Isar/parse_spec.ML
8d69da49a2aadb7415dec56ae9308d21a08973e8 ~~/src/Pure/Isar/proof.ML
530302fc1ad50354767954d751383615f0a0608f ~~/src/Pure/Isar/proof_context.ML
496b112e22bb0efd3490ee638bac778cab22a36c ~~/src/Pure/Isar/proof_display.ML
ca22dbbbdc333025bf762febed319c73866e7e59 ~~/src/Pure/Isar/proof_node.ML
9454fd8aff0ecd41373cf44db165425d1ecc6e44 ~~/src/Pure/Isar/rule_cases.ML
3734f00a262c740368f7538082d36b8b0f474b1f ~~/src/Pure/Isar/runtime.ML
52cfcee40995aead06d3c892b559747eab7ee53e ~~/src/Pure/Isar/spec_rules.ML
965acd9e9c2e9d23aad07ecf78794ccf9ea8000f ~~/src/Pure/Isar/specification.ML
1ca9f0b9a530aebdf3c17822383bf5302b803175 ~~/src/Pure/Isar/subgoal.ML
15123908c87bb5ebc45ead0b839de455858eb1b3 ~~/src/Pure/Isar/target_context.ML
01d49095f305c7bb99e88e77fe412c095c45c71c ~~/src/Pure/Isar/token.ML
ca66a9fdaf1c7500003c1b51a9bfb593323c7f76 ~~/src/Pure/Isar/toplevel.ML
c6133554a8a0dbadd7084fd365d4ede0170f8671 ~~/src/Pure/Isar/typedecl.ML
1226b7b47fb188d547c9b8f37e63e655118fe136 ~~/src/Pure/ML/exn_debugger.ML
dedc5c991fb44ecab1d47107111bd792f83ae1b2 ~~/src/Pure/ML/exn_properties.ML
eabb0e2d36816fc1ca08576364b005e05350bffa ~~/src/Pure/ML/ml_antiquotation.ML
55a233c543c04bad9c85c8cb4d451aeb5f306816 ~~/src/Pure/ML/ml_antiquotations.ML
c3bbaa40e51d40e92a94beec48f9c9afa3012aa2 ~~/src/Pure/ML/ml_compiler.ML
07bba5107f085329475729212b9d0cb9c5537517 ~~/src/Pure/ML/ml_compiler0.ML
b32af7bb576e40d8ae795b2393d1ba73425b0d31 ~~/src/Pure/ML/ml_compiler1.ML
a7f753c412e5951eb41bbce93b5c1831e7d5351d ~~/src/Pure/ML/ml_compiler2.ML
a465082ae80ad68b5bfbf7238069c3428d70a14a ~~/src/Pure/ML/ml_context.ML
6065e090d4f3e03663f2da66c4831d85ad5719c2 ~~/src/Pure/ML/ml_env.ML
35d512bf17ab6aa16aad437195a58fc16b6dae19 ~~/src/Pure/ML/ml_file.ML
e605ba067224ff419844b2d026c7d9c9ef6733a9 ~~/src/Pure/ML/ml_heap.ML
e4ec2cd3d2141e9b3cec2ac254cc5e43424fe3b1 ~~/src/Pure/ML/ml_init.ML
0be5680b1dad632e8073442c7dfa409059c1b2bf ~~/src/Pure/ML/ml_instantiate.ML
32138f3a6e7b22f6525301a051ef7a078866b7c8 ~~/src/Pure/ML/ml_lex.ML
f1f35467b47e3df3873224ccfba3ad5a19e25480 ~~/src/Pure/ML/ml_name_space.ML
ccb171b8c3706ce136587f8ffe2e8cf3fd25fe17 ~~/src/Pure/ML/ml_options.ML
106707982290df1af2386ba39045b5760dc45237 ~~/src/Pure/ML/ml_pid.ML
088127c8c85916344887bf4ddd109cf169b53f71 ~~/src/Pure/ML/ml_pp.ML
c40e93f4217efcba9e807817ada45958ba6f7de1 ~~/src/Pure/ML/ml_pretty.ML
dfcdca4d0ac3a07c1d8d941ea3703137a8efa2d9 ~~/src/Pure/ML/ml_print_depth.ML
607b6b06da26da9f12138a15bda1b4a5effb9e76 ~~/src/Pure/ML/ml_print_depth0.ML
97a01e51f50810a700e1a3cbc058f7adb2bc55bd ~~/src/Pure/ML/ml_profiling.ML
37f29f6fbc2c724b0fcf06cecec4f86b40ac52fc ~~/src/Pure/ML/ml_recursive.ML
307e9a260fa2cdc219682bff53b104d9a2957abe ~~/src/Pure/ML/ml_statistics.ML
2531efb40944080871df9c1464f1502bb2cce2fe ~~/src/Pure/ML/ml_syntax.ML
227daa0ad151b836b482911a00e4e573bcf8363e ~~/src/Pure/ML/ml_system.ML
2f53e8ff7e372e7c6a9f42d18a63f2e968aca7b5 ~~/src/Pure/ML/ml_thms.ML
5df88680e9e9717bc87c58c16a4394d5b726fa5e ~~/src/Pure/PIDE/active.ML
063aabea6a359562bc0206e2ba7ef253572ddd07 ~~/src/Pure/PIDE/byte_message.ML
d4c1f87f2e0c0f1252b94931e31ff971d4969e10 ~~/src/Pure/PIDE/command.ML
589edcc97e74f8b561cf9a3f51a76ad96d9f106f ~~/src/Pure/PIDE/command_span.ML
e7f58c7c754965b6638fb8badf6e3d8833e001c8 ~~/src/Pure/PIDE/document.ML
4bf4cbe0e549a1959b8ecfa82b3b6f913a49b748 ~~/src/Pure/PIDE/document_id.ML
90b78f510b57a9719dae9358ebe5322b0cf32e6e ~~/src/Pure/PIDE/execution.ML
25fe065f96ece466a4a176874b8b6e9f5cf56357 ~~/src/Pure/PIDE/markup.ML
4a72e5d984caf723f3ddf0b721e173fdaa14185b ~~/src/Pure/PIDE/protocol.ML
6085c589cd370295167b079e031161973a2fd1eb ~~/src/Pure/PIDE/protocol_command.ML
53742d7c23ae59bb1cde52ff9a70fd24b0f5a643 ~~/src/Pure/PIDE/protocol_message.ML
b47b868cc04236320f84dae224465154b66cf8d3 ~~/src/Pure/PIDE/query_operation.ML
10282cdad8d18a966a639502f5fe847ba58bdea0 ~~/src/Pure/PIDE/resources.ML
c32f32f33990c7a31c7e35aab3b4687b7d75a7c5 ~~/src/Pure/PIDE/session.ML
f13cd2637405c1cca730f567fde65064782d73d4 ~~/src/Pure/PIDE/xml.ML
984dc112ec098ca13ab31d33d8fd61418824cfde ~~/src/Pure/PIDE/yxml.ML
727102a627a284fcbc53cbb96ea6f41edebdd290 ~~/src/Pure/Proof/extraction.ML
ee2d9f45a68668b141da2d67f57f90668fd9320d ~~/src/Pure/Proof/proof_checker.ML
15f47a29e91edec8d90326afcf39446f1593103d ~~/src/Pure/Proof/proof_rewrite_rules.ML
f7a7e10248f84a79e82820bf2a24d3fa99e8f90d ~~/src/Pure/Proof/proof_syntax.ML
f0c7ecbc18240a126415ffffb3cc2c59de88e057 ~~/src/Pure/Pure.thy
85fdcaad624bf109f9624e330b7bcf63e8e819c1 ~~/src/Pure/ROOT.ML
48b8bdba073c09d75cd0a533adaa0d5325724d90 ~~/src/Pure/ROOT0.ML
17deb0785ded5111cf0a46696c9963e58d8ef746 ~~/src/Pure/Syntax/ast.ML
7f28507754fe56ed71a5d0bd93d377baf4172976 ~~/src/Pure/Syntax/lexicon.ML
21952dfa8abc07b2cfa1cacbb494081b05742c34 ~~/src/Pure/Syntax/local_syntax.ML
b54fc88edb7255f5f720718d4b07b79b71ce9ed2 ~~/src/Pure/Syntax/mixfix.ML
29baddfdf89f8b711a28dd8834628d085bac8151 ~~/src/Pure/Syntax/parser.ML
8eafbd813906fb5c6ba5ffc99a24f404de52197c ~~/src/Pure/Syntax/printer.ML
720b31a896a40b66832345fb584e34fde997f057 ~~/src/Pure/Syntax/simple_syntax.ML
5c2a9fd6ce7393b89b59bc006a0c9c1185a8fb05 ~~/src/Pure/Syntax/syntax.ML
59ad26e85df1ec2a216a8c451260975b987e5eea ~~/src/Pure/Syntax/syntax_ext.ML
6b67c207f7740b0f0df2bdd8aa73eb27a2a6ce6a ~~/src/Pure/Syntax/syntax_phases.ML
07b5dda36d69cd1829bd8aa31e19b5e28bf3b0b5 ~~/src/Pure/Syntax/syntax_trans.ML
3bd55164187cb504b23e305488300ca4f9a0a843 ~~/src/Pure/Syntax/term_position.ML
469039221a690286ae653a4e411903d547677806 ~~/src/Pure/Syntax/type_annotation.ML
93ccdaa0ae2d6e54548ed57c9246f397eac1763a ~~/src/Pure/System/bash.ML
288a1a9f152f5ff49028e2fcf74cf130ddc84949 ~~/src/Pure/System/command_line.ML
b29758d0981820364779c078d238c2b24a9d9461 ~~/src/Pure/System/isabelle_process.ML
7cc9f6abd0c048dd537d2bb009a37c3ad4a56c1c ~~/src/Pure/System/isabelle_system.ML
b99be2c4000d3a9d750711d754626f1b634a481d ~~/src/Pure/System/isabelle_tool.ML
8bbad21a931aa633f740a371fe256941adb960a6 ~~/src/Pure/System/java.ML
7bc10bb51c096ec8ad6b8985d71fb6e6a4cc2132 ~~/src/Pure/System/message_channel.ML
81dfe82a8d1e93e552d8b2f54dc645180b3b7488 ~~/src/Pure/System/options.ML
dd5c5f0371d4c32995579d2be41f6e4756d7e0b0 ~~/src/Pure/System/process_result.ML
ed03b0664edc84034dcbf703b1d5552dedca812c ~~/src/Pure/System/scala.ML
a349cc5d8c4f09763ca4c2a3311a1e4b07c72532 ~~/src/Pure/System/scala_compiler.ML
8156fbed39461d0a4a72a733276d536b5f87a15d ~~/src/Pure/Thy/bibtex.ML
8493f21b415ec8ba18dfd8052928cedc68ee552e ~~/src/Pure/Thy/document_antiquotation.ML
7bb25bed921c5b5fd3d36bcf9d195a0b9d37ca9a ~~/src/Pure/Thy/document_antiquotations.ML
3619fa860fed952a1034b4e2b30c500fc58f05db ~~/src/Pure/Thy/document_marker.ML
09bdc834db039ca084fd8da39354757810b56d96 ~~/src/Pure/Thy/document_output.ML
1b86bd43d86021d318329433f969a2b33b9dac3f ~~/src/Pure/Thy/document_source.ML
a7a01279ded44eab14407c555b35c272d40e5e26 ~~/src/Pure/Thy/export.ML
ab83a6aaca88c15a2f4b32353bfc1ef161aef420 ~~/src/Pure/Thy/export_theory.ML
20e1551820db3d35d477cfc075f9f60943323ab6 ~~/src/Pure/Thy/latex.ML
aa524a09cdfff619020b366f830b179862de5a12 ~~/src/Pure/Thy/markdown.ML
e008cec34267fd1de9e7804f377ffae3814dc8e3 ~~/src/Pure/Thy/sessions.ML
9bac53fa6fa66f85b23e697c548f5da463abf401 ~~/src/Pure/Thy/term_style.ML
fb8a4a34e4e3f642e2442e7c6b0c27c9e0a7151e ~~/src/Pure/Thy/thy_element.ML
14034e3744b36c3a74a12935004a6dc0862a8f17 ~~/src/Pure/Thy/thy_header.ML
d087f00c0eef12477759480ccda278bf1cf94f7a ~~/src/Pure/Thy/thy_info.ML
163be1282c0e0a6181141e9f0d569fe1a3c19178 ~~/src/Pure/Tools/build.ML
202c4fd756e8a7f7f6e8683f1b993c5696399917 ~~/src/Pure/Tools/class_deps.ML
dcf80294bf3afca130da926c2d066716e2c94546 ~~/src/Pure/Tools/debugger.ML
f99c29dec00e92ac05562ce08ce6e601c68b5f17 ~~/src/Pure/Tools/doc.ML
147bca00e6d281a45af02293c6a5c44e17ca7fd4 ~~/src/Pure/Tools/find_consts.ML
f4d64978b78bbb1ce6d3ac976ea3ae659ef78aa6 ~~/src/Pure/Tools/find_theorems.ML
578944df0636eb8afa92a2cc29091d8532bdd3c2 ~~/src/Pure/Tools/generated_files.ML
09087576c696b6e58a39848f236d29c600707033 ~~/src/Pure/Tools/ghc.ML
8f0353da5c81ca9172f2881fc84237bf7cbaa01a ~~/src/Pure/Tools/jedit.ML
2d391d7bc54008f9b9f0d54cc1bbe554d24043ce ~~/src/Pure/Tools/named_theorems.ML
b21a1cfed6722605f54b5c0727258aac2dca3992 ~~/src/Pure/Tools/named_thms.ML
fef1d70ab65787db979f14c13ebb8bf09355b28d ~~/src/Pure/Tools/plugin.ML
681ac9843fe9cd1cd349fcbfe7c6d5b2b9ad6e0e ~~/src/Pure/Tools/print_operation.ML
0c24deb6ca3462e11532d2b0b16359d54c99326b ~~/src/Pure/Tools/prismjs.ML
7a3a9e4c90cef918588e235e93f0b850cc3de9cb ~~/src/Pure/Tools/rail.ML
bce823e0579715bec9adfb162a9e863d16217e3e ~~/src/Pure/Tools/rule_insts.ML
2a20e2e0f9a58b0b494f044486841ee3162fb7c6 ~~/src/Pure/Tools/simplifier_trace.ML
d007e80fc985e6b554af8b149e5f6b9a48440751 ~~/src/Pure/Tools/thy_deps.ML
129ad332b3a7b507cb9ac77a900a7b428243257b ~~/src/Pure/assumption.ML
99e360bdbc97636644100845686adf1f1842e777 ~~/src/Pure/axclass.ML
abfd0de922a15f8954ef91d000967b44a02dde99 ~~/src/Pure/config.ML
e3cfee2e41edd32e165927ddd621a8fc940a530c ~~/src/Pure/conjunction.ML
8e8a775ccd51d4a654ed3ae4dd044d36eea936b0 ~~/src/Pure/consts.ML
18c46e01823b18d62edf2562fd90ba495445f016 ~~/src/Pure/context.ML
1b08ee0296a700a438dc5cff018d9848b9415e54 ~~/src/Pure/context_position.ML
8a28f1de59a20ef08ebc6ec713b0463391036202 ~~/src/Pure/context_tactic.ML
6fd5b27d6c00d915ad58b3a43d4ccaa0a0230ba0 ~~/src/Pure/conv.ML
e3e1b5c2b1f392f41af5d6aa2f7d5a70fade1620 ~~/src/Pure/cterm_items.ML
c694df79970ecb8d7ff0c18c2535a4197f94c62f ~~/src/Pure/defs.ML
bd0df4c133bfaf0e31c1c37bdd70b774845c2bd9 ~~/src/Pure/drule.ML
6aceceb10c357f1e60014000c61f16aadb85ab6e ~~/src/Pure/envir.ML
5224d7cf4a18a04b0af436987fce290e5a867113 ~~/src/Pure/facts.ML
fae207874b41d538731013270e972b1908ebd467 ~~/src/Pure/global_theory.ML
4bb147680a63e68d241d497e9a2612a93b115628 ~~/src/Pure/goal.ML
798c9fd569fbeabffdcce2b32cb17d61a593f645 ~~/src/Pure/goal_display.ML
e83ba2670c552dea3a5bbf3b1f2f4de1694d19c3 ~~/src/Pure/item_net.ML
e306b0e8cb116faae7d88659bf538c0af6600433 ~~/src/Pure/library.ML
fdcb90714dabda6fe2384b7ec6a6211c18a12ef3 ~~/src/Pure/logic.ML
0e529cfa40cf501f004d691db353b2b32ad1e05a ~~/src/Pure/more_pattern.ML
69cdc1b5f3e83aac68edd9260af662696d6c644c ~~/src/Pure/more_thm.ML
2f769445fa015b9264012c16d027044b45023a97 ~~/src/Pure/more_unify.ML
b75caaefb22376c6f484e2022756e87c4c817bb2 ~~/src/Pure/morphism.ML
d1b5959180aff47512ab4be50f4edbdfca890b66 ~~/src/Pure/name.ML
81e120b33435a8ef1ef05dd0a2530e83cfec9ca7 ~~/src/Pure/net.ML
5dde4e7011a8df535f240525e570aa772d37560f ~~/src/Pure/par_tactical.ML
128bd15a02b902b9fca342315cea8252973acaed ~~/src/Pure/pattern.ML
26a7a88908fffd2bbdaafd4d1efc47d529f6898b ~~/src/Pure/primitive_defs.ML
7404a4d4025c6f947a638cf4f190c4151d3fcf5c ~~/src/Pure/proofterm.ML
9733252b5dff04f64da33b38a21f2a0c6ca3927a ~~/src/Pure/pure_syn.ML
01b9a683b55fda86f58300af3c5987a4b2196701 ~~/src/Pure/pure_thy.ML
2330daa5f2e24cb2cd8f7facddfcdd69eba3dc56 ~~/src/Pure/raw_simplifier.ML
d8e5d56b207e007ec696868bbe230b2aa70f834e ~~/src/Pure/search.ML
08c1186951fe80ca8646456ea3e91d3f489209d5 ~~/src/Pure/sign.ML
4e6530f1a6e4ce76c97c41428be30857a79838d2 ~~/src/Pure/simplifier.ML
896ba3d4ba4c19c8a240cac0a69e675736a36914 ~~/src/Pure/skip_proof.ML
7fe8a36dd00b77508050d39bef533c9bb683fff9 ~~/src/Pure/soft_type_system.ML
3748e50e70fa6c1a2837c77fae337b36e3ccd295 ~~/src/Pure/sorts.ML
73f57c5bd22f3313db0e8fd3a6e2f412336ab6ec ~~/src/Pure/tactic.ML
3a02b8be8d82e4f68d77430bb8babd001cf641a9 ~~/src/Pure/tactical.ML
6248d5307266d86c66dfc0e2e515f3bc733bad98 ~~/src/Pure/term.ML
5186b979f954c303652514b56b21a02a245751f1 ~~/src/Pure/term_items.ML
ff5c6b1102c66c639575764ff3ef59152411d03f ~~/src/Pure/term_ord.ML
88bb43e18f4224ef207d1ab0689f3bb536487ca8 ~~/src/Pure/term_sharing.ML
f874d46d8c272d8f2ea9c43a068d42b775d97a81 ~~/src/Pure/term_subst.ML
960e223fbec5f0e953fdcba8a97ae7ef4d5cc415 ~~/src/Pure/term_xml.ML
5301eb946afd88d9f0a88c0bdd86f2a892b53d81 ~~/src/Pure/theory.ML
ce3a503ef6c3d9a2130334e768f636d8bab3ce47 ~~/src/Pure/thm.ML
0a645a6222e7e54a87c9af319487a7d298bd37c5 ~~/src/Pure/thm_deps.ML
0934782140ded8ebe8342192ecdc7ee3f1997e6d ~~/src/Pure/thm_name.ML
0ea94c480568b8dcf256f560d7196bd9d9595aa5 ~~/src/Pure/type.ML
82f8863240fb0885d5d1f93ac0df7a8d53a097e2 ~~/src/Pure/type_infer.ML
17aa4d0bc989ade05f92f77499b6f299442aafd3 ~~/src/Pure/type_infer_context.ML
2ce315f1b1c0e771e1bc06be7bed2d53bc78149d ~~/src/Pure/unify.ML
ac9bcfe3982550a519923be37f33cff4148abd35 ~~/src/Pure/variable.ML
62c28e5ccb473bc5eb3b674e4debc873b7cd50e4 ~~/src/Tools/IsaPlanner/isand.ML
33c37ffe98516cabcca86dd412495e057cbb61bc ~~/src/Tools/IsaPlanner/rw_inst.ML
793e0012ce134159ebf0f52633f4ee2c60b00c53 ~~/src/Tools/IsaPlanner/zipper.ML
944d5fdf5467daed2986de1e8420cf964c9df7b8 ~~/src/Tools/atomize_elim.ML
d865dafb0804ec845e91238b99c21a494e8e0401 ~~/src/Tools/case_product.ML
14b9c6e02786d1399e18d8d1df4dbeacb8756ea4 ~~/src/Tools/eqsubst.ML
700cdcd19197702911ef1a2617f318f39c8b643d ~~/src/Tools/induct.ML
14db55975ce70793e1f28e49981ebc12bf712aaa ~~/src/Tools/intuitionistic.ML
63cca5b678da86f6a6c46e229db8dd45b4bfcaba ~~/src/Tools/misc_legacy.ML
f6bf49589bc66db14a6c8b5cfa468392b6ad28b8 ~~/src/Tools/project_rule.ML
54790bb695682edbb13ab5f397b0d4fd55de68be ~~/src/ZF/AC.thy
d3975a35609a3224ea3d5323cf39237d0064b763 ~~/src/ZF/Arith.thy
e9cbacafe33aa76857e30a5f86e62ed52d463423 ~~/src/ZF/ArithSimp.thy
79bceba2bf0747d886ca978756fbad682f30388f ~~/src/ZF/Bin.thy
73ebe355cd840237427bcd1d6da4acb0db5976b0 ~~/src/ZF/Bool.thy
f2aba3dea610f42d1d90aa203c22835d2eab789d ~~/src/ZF/Cardinal.thy
4a45bbc0b3859af21a32e5cb75a1d3882330aad3 ~~/src/ZF/CardinalArith.thy
3fecdea91f68ca19f3ede64d0c1e69cf8539ad58 ~~/src/ZF/Cardinal_AC.thy
922240e369d26c0207842490213ebebd1b43a11e ~~/src/ZF/Datatype.thy
44c70208f3f74675b5e7fe6bd294097be7d965d8 ~~/src/ZF/Epsilon.thy
cbd4ac2463045ac08c859a9230a48b54cd9821f7 ~~/src/ZF/EquivClass.thy
5769e2ac971c77fde455ddd0cafe8ebea5cacbf7 ~~/src/ZF/Finite.thy
93446a597ceda79b612b3b741ce94f5160b33910 ~~/src/ZF/Fixedpt.thy
f5a929563212c8642279cd620e1fd055f0e632f5 ~~/src/ZF/Inductive.thy
1e65fd3cfadda0aac7f2b3e99ccacdd456c09cb3 ~~/src/ZF/InfDatatype.thy
d1ae3b892cb818bc07e0c21c997480642b3af440 ~~/src/ZF/Int.thy
18fff92af7e229bb3541b921344b8a4625175f22 ~~/src/ZF/IntDiv.thy
26ab2c9f5db2bd547fcf1060116314f2b928a1ad ~~/src/ZF/List.thy
c51cdaff3f10e9e5dd995da5af14c89483dc2445 ~~/src/ZF/Nat.thy
2ecc73cf43d8a5c63000f06875155ed5ad73c02e ~~/src/ZF/OrdQuant.thy
ff8d0201e29cac0c98e24040e677ccabdbbeaa63 ~~/src/ZF/Order.thy
61265c52e488f9ec8dc87a54d4bd81e5e099bce1 ~~/src/ZF/OrderArith.thy
e7f8036a239b050e55774d1f4977f070ce719538 ~~/src/ZF/OrderType.thy
d20c28c179b9dd2615ea17329b0fbdeb97c61d4c ~~/src/ZF/Ordinal.thy
8a7edca164cf873447ccbd55d9729382623823e0 ~~/src/ZF/Perm.thy
4d26c4208483f5c12187c50c1ae939f015063fd6 ~~/src/ZF/QPair.thy
74574d4e2b817129cd1c4be77ef3d5c646c7f8b3 ~~/src/ZF/QUniv.thy
e4a656c486d93cb9a35917d6e128009c745773a9 ~~/src/ZF/Sum.thy
812709eeb42682383f8bcdeef67e1078895b6f23 ~~/src/ZF/Tools/cartprod.ML
198772831774381d3d604f8d063251a912d2db39 ~~/src/ZF/Tools/datatype_package.ML
b2e087ab7f27aac188ebde04abe0d3f64cb2c029 ~~/src/ZF/Tools/ind_cases.ML
3b12a05e67f104601ad3afe3f7ce21f499781d2e ~~/src/ZF/Tools/induct_tacs.ML
11bd580fae1e143a6a47dedd14fefd0d23df904e ~~/src/ZF/Tools/inductive_package.ML
0f275d2c896fe9f267cb151f550c85367f18b4d4 ~~/src/ZF/Tools/numeral_syntax.ML
5aad87d5bb6f6c7b4f4573e39fe96396ff78d6f8 ~~/src/ZF/Tools/primrec_package.ML
344bf92e00b4e296df6e52fe318bcc84fda62683 ~~/src/ZF/Tools/typechk.ML
7d35c4336ac3ebc46d502fffb37ecf2630f43ac0 ~~/src/ZF/Trancl.thy
0d7d3f6d224b0453240d037eb17fdfbbd2ee3597 ~~/src/ZF/Univ.thy
4e0f9b002d1156b6ab0cf365afee47dbace86914 ~~/src/ZF/WF.thy
307efe9622dc1ceb9ba637a06ef3aa700ac8b9eb ~~/src/ZF/ZF.thy
6af354a18cb6a6850e2f220a90b2fb9181af9f1a ~~/src/ZF/ZFC.thy
49acb4339c076c411ce2748b726ea8d83d511ed4 ~~/src/ZF/ZF_Base.thy
5b4708b1cf51e45862c519248076a1abda7fed0e ~~/src/ZF/Zorn.thy
451a705fbb3bda95bd4812ad2c7be6780f2d702b ~~/src/ZF/arith_data.ML
b404f0d0ac55c871253c7133559af5d08e659365 ~~/src/ZF/document/root.tex
af31ed5a16108e13e312b4ca3c065867ef8a1f39 ~~/src/ZF/equalities.thy
bf729a9c880ee60604f55bd7e8fc663e34ad4025 ~~/src/ZF/func.thy
9bd907309451bfc52f9c3eae02237499a23c97ca ~~/src/ZF/ind_syntax.ML
c83f4c223b14a4ed3239e10b32200ae1ad59b430 ~~/src/ZF/int_arith.ML
0de4a46674bd83c3438c97d651722f56a2684091 ~~/src/ZF/pair.thy
9deb894c5b5a4ab761867d1db692335681b76e08 ~~/src/ZF/simpdata.ML
5628d11f5cca7dfd309ca8cfee8fbc0d2abd92b3 ~~/src/ZF/upair.thy


