equal
deleted
inserted
replaced
1 (* Title: HOL/HOL.thy |
1 (* Title: HOL/HOL.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson |
2 Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson |
4 *) |
3 *) |
5 |
4 |
6 header {* The basis of Higher-Order Logic *} |
5 header {* The basis of Higher-Order Logic *} |
7 |
6 |
8 theory HOL |
7 theory HOL |
9 imports Pure |
8 imports Pure |
10 uses |
9 uses |
11 ("hologic.ML") |
10 ("Tools/hologic.ML") |
12 "~~/src/Tools/IsaPlanner/zipper.ML" |
11 "~~/src/Tools/IsaPlanner/zipper.ML" |
13 "~~/src/Tools/IsaPlanner/isand.ML" |
12 "~~/src/Tools/IsaPlanner/isand.ML" |
14 "~~/src/Tools/IsaPlanner/rw_tools.ML" |
13 "~~/src/Tools/IsaPlanner/rw_tools.ML" |
15 "~~/src/Tools/IsaPlanner/rw_inst.ML" |
14 "~~/src/Tools/IsaPlanner/rw_inst.ML" |
16 "~~/src/Provers/project_rule.ML" |
15 "~~/src/Provers/project_rule.ML" |
20 "~~/src/Provers/blast.ML" |
19 "~~/src/Provers/blast.ML" |
21 "~~/src/Provers/clasimp.ML" |
20 "~~/src/Provers/clasimp.ML" |
22 "~~/src/Provers/coherent.ML" |
21 "~~/src/Provers/coherent.ML" |
23 "~~/src/Provers/eqsubst.ML" |
22 "~~/src/Provers/eqsubst.ML" |
24 "~~/src/Provers/quantifier1.ML" |
23 "~~/src/Provers/quantifier1.ML" |
25 ("simpdata.ML") |
24 ("Tools/simpdata.ML") |
26 "~~/src/Tools/random_word.ML" |
25 "~~/src/Tools/random_word.ML" |
27 "~~/src/Tools/atomize_elim.ML" |
26 "~~/src/Tools/atomize_elim.ML" |
28 "~~/src/Tools/induct.ML" |
27 "~~/src/Tools/induct.ML" |
29 ("~~/src/Tools/induct_tacs.ML") |
28 ("~~/src/Tools/induct_tacs.ML") |
30 "~~/src/Tools/code/code_name.ML" |
29 "~~/src/Tools/code/code_name.ML" |
799 |
798 |
800 lemmas [trans] = trans |
799 lemmas [trans] = trans |
801 and [sym] = sym not_sym |
800 and [sym] = sym not_sym |
802 and [Pure.elim?] = iffD1 iffD2 impE |
801 and [Pure.elim?] = iffD1 iffD2 impE |
803 |
802 |
804 use "hologic.ML" |
803 use "Tools/hologic.ML" |
805 |
804 |
806 |
805 |
807 subsubsection {* Atomizing meta-level connectives *} |
806 subsubsection {* Atomizing meta-level connectives *} |
808 |
807 |
809 axiomatization where |
808 axiomatization where |
1283 |
1282 |
1284 lemma ex_comm: |
1283 lemma ex_comm: |
1285 "(\<exists>x y. P x y) = (\<exists>y x. P x y)" |
1284 "(\<exists>x y. P x y) = (\<exists>y x. P x y)" |
1286 by blast |
1285 by blast |
1287 |
1286 |
1288 use "simpdata.ML" |
1287 use "Tools/simpdata.ML" |
1289 ML {* open Simpdata *} |
1288 ML {* open Simpdata *} |
1290 |
1289 |
1291 setup {* |
1290 setup {* |
1292 Simplifier.method_setup Splitter.split_modifiers |
1291 Simplifier.method_setup Splitter.split_modifiers |
1293 #> Simplifier.map_simpset (K Simpdata.simpset_simprocs) |
1292 #> Simplifier.map_simpset (K Simpdata.simpset_simprocs) |