/src/Pure/
drwxr-xr-x [up]
drwxr-xr-x Admin
drwxr-xr-x Build
drwxr-xr-x Concurrent
drwxr-xr-x Examples
drwxr-xr-x GUI
drwxr-xr-x General
drwxr-xr-x Isar
drwxr-xr-x ML
drwxr-xr-x PIDE
drwxr-xr-x Proof
drwxr-xr-x Syntax
drwxr-xr-x System
drwxr-xr-x Thy
drwxr-xr-x Tools
drwxr-xr-x ex
-rw-r--r-- 2024-10-22 12:28 +0200 1135 ML_Bootstrap.thy
-rw-r--r-- 2024-10-22 12:28 +0200 62343 Pure.thy
-rw-r--r-- 2024-10-22 12:28 +0200 502 README
-rw-r--r-- 2024-10-22 12:28 +0200 844 ROOT
-rw-r--r-- 2024-10-22 12:28 +0200 9372 ROOT.ML
-rw-r--r-- 2024-10-22 12:28 +0200 1171 ROOT.scala
-rw-r--r-- 2024-10-22 12:28 +0200 326 ROOT0.ML
-rw-r--r-- 2024-10-22 12:28 +0200 644 Sessions.thy
-rw-r--r-- 2024-10-22 12:28 +0200 4945 assumption.ML
-rw-r--r-- 2024-10-22 12:28 +0200 16427 axclass.ML
-rw-r--r-- 2024-10-22 12:28 +0200 7290 config.ML
-rw-r--r-- 2024-10-22 12:28 +0200 5503 conjunction.ML
-rw-r--r-- 2024-10-22 12:28 +0200 12652 consts.ML
-rw-r--r-- 2024-10-22 12:28 +0200 24603 context.ML
-rw-r--r-- 2024-10-22 12:28 +0200 3945 context_position.ML
-rw-r--r-- 2024-10-22 12:28 +0200 2927 context_tactic.ML
-rw-r--r-- 2024-10-22 12:28 +0200 7123 conv.ML
-rw-r--r-- 2024-10-22 12:28 +0200 1104 cterm_items.ML
-rw-r--r-- 2024-10-22 12:28 +0200 9450 defs.ML
-rw-r--r-- 2024-10-22 12:28 +0200 29821 drule.ML
-rw-r--r-- 2024-10-22 12:28 +0200 14110 envir.ML
-rw-r--r-- 2024-10-22 12:28 +0200 9690 facts.ML
-rw-r--r-- 2024-10-22 12:28 +0200 14364 global_theory.ML
-rw-r--r-- 2024-10-22 12:28 +0200 11435 goal.ML
-rw-r--r-- 2024-10-22 12:28 +0200 4044 goal_display.ML
-rw-r--r-- 2024-10-22 12:28 +0200 2476 item_net.ML
-rw-r--r-- 2024-10-22 12:28 +0200 34080 library.ML
-rw-r--r-- 2024-10-22 12:28 +0200 10007 library.scala
-rw-r--r-- 2024-10-22 12:28 +0200 23678 logic.ML
-rw-r--r-- 2024-10-22 12:28 +0200 4391 more_pattern.ML
-rw-r--r-- 2024-10-22 12:28 +0200 25174 more_thm.ML
-rw-r--r-- 2024-10-22 12:28 +0200 3206 more_unify.ML
-rw-r--r-- 2024-10-22 12:28 +0200 9874 morphism.ML
-rw-r--r-- 2024-10-22 12:28 +0200 5726 name.ML
-rw-r--r-- 2024-10-22 12:28 +0200 185 name.scala
-rw-r--r-- 2024-10-22 12:28 +0200 9636 net.ML
-rw-r--r-- 2024-10-22 12:28 +0200 1870 par_tactical.ML
-rw-r--r-- 2024-10-22 12:28 +0200 15784 pattern.ML
-rw-r--r-- 2024-10-22 12:28 +0200 3202 primitive_defs.ML
-rw-r--r-- 2024-10-22 12:28 +0200 90490 proofterm.ML
-rw-r--r-- 2024-10-22 12:28 +0200 1769 pure_syn.ML
-rw-r--r-- 2024-10-22 12:28 +0200 18159 pure_thy.ML
-rw-r--r-- 2024-10-22 12:28 +0200 745 pure_thy.scala
-rw-r--r-- 2024-10-22 12:28 +0200 60193 raw_simplifier.ML
-rw-r--r-- 2024-10-22 12:28 +0200 9434 search.ML
-rw-r--r-- 2024-10-22 12:28 +0200 21339 sign.ML
-rw-r--r-- 2024-10-22 12:28 +0200 20726 simplifier.ML
-rw-r--r-- 2024-10-22 12:28 +0200 1086 skip_proof.ML
-rw-r--r-- 2024-10-22 12:28 +0200 2182 soft_type_system.ML
-rw-r--r-- 2024-10-22 12:28 +0200 18215 sorts.ML
-rw-r--r-- 2024-10-22 12:28 +0200 13363 tactic.ML
-rw-r--r-- 2024-10-22 12:28 +0200 11261 tactical.ML
-rw-r--r-- 2024-10-22 12:28 +0200 39075 term.ML
-rw-r--r-- 2024-10-22 12:28 +0200 9717 term.scala
-rw-r--r-- 2024-10-22 12:28 +0200 6401 term_items.ML
-rw-r--r-- 2024-10-22 12:28 +0200 7057 term_ord.ML
-rw-r--r-- 2024-10-22 12:28 +0200 2185 term_sharing.ML
-rw-r--r-- 2024-10-22 12:28 +0200 9489 term_subst.ML
-rw-r--r-- 2024-10-22 12:28 +0200 2578 term_xml.ML
-rw-r--r-- 2024-10-22 12:28 +0200 3789 term_xml.scala
-rw-r--r-- 2024-10-22 12:28 +0200 13690 theory.ML
-rw-r--r-- 2024-10-22 12:28 +0200 100435 thm.ML
-rw-r--r-- 2024-10-22 12:28 +0200 4970 thm_deps.ML
-rw-r--r-- 2024-10-22 12:28 +0200 3265 thm_name.ML
-rw-r--r-- 2024-10-22 12:28 +0200 1426 thm_name.scala
-rw-r--r-- 2024-10-22 12:28 +0200 25260 type.ML
-rw-r--r-- 2024-10-22 12:28 +0200 3699 type_infer.ML
-rw-r--r-- 2024-10-22 12:28 +0200 11079 type_infer_context.ML
-rw-r--r-- 2024-10-22 12:28 +0200 27344 unify.ML
-rw-r--r-- 2024-10-22 12:28 +0200 1167 update.scala
-rw-r--r-- 2024-10-22 12:28 +0200 28933 variable.ML
-rw-r--r-- 2024-10-22 12:28 +0200 59686 zterm.ML