equal
deleted
inserted
replaced
10 ("Tools/hologic.ML") |
10 ("Tools/hologic.ML") |
11 "~~/src/Tools/IsaPlanner/zipper.ML" |
11 "~~/src/Tools/IsaPlanner/zipper.ML" |
12 "~~/src/Tools/IsaPlanner/isand.ML" |
12 "~~/src/Tools/IsaPlanner/isand.ML" |
13 "~~/src/Tools/IsaPlanner/rw_tools.ML" |
13 "~~/src/Tools/IsaPlanner/rw_tools.ML" |
14 "~~/src/Tools/IsaPlanner/rw_inst.ML" |
14 "~~/src/Tools/IsaPlanner/rw_inst.ML" |
|
15 "~~/src/Tools/intuitionistic.ML" |
15 "~~/src/Tools/project_rule.ML" |
16 "~~/src/Tools/project_rule.ML" |
16 "~~/src/Provers/hypsubst.ML" |
17 "~~/src/Provers/hypsubst.ML" |
17 "~~/src/Provers/splitter.ML" |
18 "~~/src/Provers/splitter.ML" |
18 "~~/src/Provers/classical.ML" |
19 "~~/src/Provers/classical.ML" |
19 "~~/src/Provers/blast.ML" |
20 "~~/src/Provers/blast.ML" |
36 "~~/src/Tools/code/code_ml.ML" |
37 "~~/src/Tools/code/code_ml.ML" |
37 "~~/src/Tools/code/code_haskell.ML" |
38 "~~/src/Tools/code/code_haskell.ML" |
38 "~~/src/Tools/nbe.ML" |
39 "~~/src/Tools/nbe.ML" |
39 ("Tools/recfun_codegen.ML") |
40 ("Tools/recfun_codegen.ML") |
40 begin |
41 begin |
|
42 |
|
43 setup {* Intuitionistic.method_setup "iprover" *} |
|
44 |
41 |
45 |
42 subsection {* Primitive logic *} |
46 subsection {* Primitive logic *} |
43 |
47 |
44 subsubsection {* Core syntax *} |
48 subsubsection {* Core syntax *} |
45 |
49 |