aboutsummaryrefslogtreecommitdiff
path: root/spartan/core
ModeNameSize
-rw-r--r--Spartan.thy18134logplain
-rw-r--r--cases.ML1136logplain
-rw-r--r--congruence.ML2399logplain
-rw-r--r--context_tactical.ML5218logplain
-rw-r--r--elimination.ML1433logplain
-rw-r--r--eqsubst.ML16336logplain
-rw-r--r--equality.ML2931logplain
-rw-r--r--focus.ML4598logplain
-rw-r--r--goals.ML7571logplain
-rw-r--r--implicits.ML2507logplain
-rw-r--r--lib.ML3748logplain
-rw-r--r--rewrite.ML17731logplain
-rw-r--r--tactics.ML6430logplain
-rw-r--r--typechecking.ML2788logplain