aboutsummaryrefslogtreecommitdiff
path: root/mltt/core
ModeNameSize
-rw-r--r--MLTT.thy18864logplain
-rw-r--r--calc.ML2544logplain
-rw-r--r--cases.ML1136logplain
-rw-r--r--comp.ML17801logplain
-rw-r--r--context_facts.ML2946logplain
-rw-r--r--context_tactical.ML9185logplain
-rw-r--r--elaborated_statement.ML18819logplain
-rw-r--r--elaboration.ML3444logplain
-rw-r--r--elimination.ML1431logplain
-rw-r--r--eqsubst.ML16344logplain
-rw-r--r--focus.ML5766logplain
-rw-r--r--goals.ML8792logplain
-rw-r--r--implicits.ML2589logplain
-rw-r--r--lib.ML6008logplain
-rw-r--r--tactics.ML6509logplain
-rw-r--r--types.ML3646logplain