/src/Pure/
drwxr-xr-x [up]
drwxr-xr-x Concurrent
drwxr-xr-x General
drwxr-xr-x Isar
drwxr-xr-x ML
drwxr-xr-x ML-Systems
drwxr-xr-x PIDE
drwxr-xr-x Proof
drwxr-xr-x ProofGeneral
drwxr-xr-x Syntax
drwxr-xr-x System
drwxr-xr-x Thy
drwxr-xr-x Tools
-rw-r--r-- 2010-12-20 07:50 -0800 6440 IsaMakefile
-rw-r--r-- 2010-12-20 07:50 -0800 2232 Pure.thy
-rw-r--r-- 2010-12-20 07:50 -0800 516 README
-rw-r--r-- 2010-12-20 07:50 -0800 6454 ROOT.ML
-rw-r--r-- 2010-12-20 07:50 -0800 3441 assumption.ML
-rw-r--r-- 2010-12-20 07:50 -0800 23400 axclass.ML
-rwxr-xr-x 2010-12-20 07:50 -0800 2507 build-jars
-rw-r--r-- 2010-12-20 07:50 -0800 40194 codegen.ML
-rw-r--r-- 2010-12-20 07:50 -0800 4550 config.ML
-rw-r--r-- 2010-12-20 07:50 -0800 4643 conjunction.ML
-rw-r--r-- 2010-12-20 07:50 -0800 10384 consts.ML
-rw-r--r-- 2010-12-20 07:50 -0800 19835 context.ML
-rw-r--r-- 2010-12-20 07:50 -0800 1212 context_position.ML
-rw-r--r-- 2010-12-20 07:50 -0800 6115 conv.ML
-rw-r--r-- 2010-12-20 07:50 -0800 7273 defs.ML
-rw-r--r-- 2010-12-20 07:50 -0800 9387 display.ML
-rw-r--r-- 2010-12-20 07:50 -0800 33238 drule.ML
-rw-r--r-- 2010-12-20 07:50 -0800 12776 envir.ML
-rw-r--r-- 2010-12-20 07:50 -0800 6619 facts.ML
-rw-r--r-- 2010-12-20 07:50 -0800 7370 global_theory.ML
-rw-r--r-- 2010-12-20 07:50 -0800 10433 goal.ML
-rw-r--r-- 2010-12-20 07:50 -0800 5189 goal_display.ML
-rw-r--r-- 2010-12-20 07:50 -0800 1407 interpretation.ML
-rw-r--r-- 2010-12-20 07:50 -0800 1789 item_net.ML
-rw-r--r-- 2010-12-20 07:50 -0800 32447 library.ML
-rw-r--r-- 2010-12-20 07:50 -0800 3957 library.scala
-rw-r--r-- 2010-12-20 07:50 -0800 19147 logic.ML
-rwxr-xr-x 2010-12-20 07:50 -0800 2446 mk
-rw-r--r-- 2010-12-20 07:50 -0800 14350 more_thm.ML
-rw-r--r-- 2010-12-20 07:50 -0800 2583 morphism.ML
-rw-r--r-- 2010-12-20 07:50 -0800 4883 name.ML
-rw-r--r-- 2010-12-20 07:50 -0800 9699 net.ML
-rw-r--r-- 2010-12-20 07:50 -0800 3631 old_term.ML
-rw-r--r-- 2010-12-20 07:50 -0800 19935 pattern.ML
-rw-r--r-- 2010-12-20 07:50 -0800 3031 primitive_defs.ML
-rw-r--r-- 2010-12-20 07:50 -0800 60886 proofterm.ML
-rw-r--r-- 2010-12-20 07:50 -0800 2130 pure_setup.ML
-rw-r--r-- 2010-12-20 07:50 -0800 8863 pure_thy.ML
-rw-r--r-- 2010-12-20 07:50 -0800 53962 raw_simplifier.ML
-rw-r--r-- 2010-12-20 07:50 -0800 11639 search.ML
-rw-r--r-- 2010-12-20 07:50 -0800 20502 sign.ML
-rw-r--r-- 2010-12-20 07:50 -0800 13731 simplifier.ML
-rw-r--r-- 2010-12-20 07:50 -0800 16847 sorts.ML
-rw-r--r-- 2010-12-20 07:50 -0800 5114 subgoal.ML
-rw-r--r-- 2010-12-20 07:50 -0800 13358 tactic.ML
-rw-r--r-- 2010-12-20 07:50 -0800 14134 tactical.ML
-rw-r--r-- 2010-12-20 07:50 -0800 35264 term.ML
-rw-r--r-- 2010-12-20 07:50 -0800 7295 term_ord.ML
-rw-r--r-- 2010-12-20 07:50 -0800 6546 term_subst.ML
-rw-r--r-- 2010-12-20 07:50 -0800 9683 theory.ML
-rw-r--r-- 2010-12-20 07:50 -0800 62049 thm.ML
-rw-r--r-- 2010-12-20 07:50 -0800 23595 type.ML
-rw-r--r-- 2010-12-20 07:50 -0800 11897 type_infer.ML
-rw-r--r-- 2010-12-20 07:50 -0800 29804 unify.ML
-rw-r--r-- 2010-12-20 07:50 -0800 19456 variable.ML