equal
deleted
inserted
replaced
6 Combination of classical reasoner and simplifier (depends on |
6 Combination of classical reasoner and simplifier (depends on |
7 simplifier.ML, splitter.ML classical.ML, blast.ML). |
7 simplifier.ML, splitter.ML classical.ML, blast.ML). |
8 *) |
8 *) |
9 |
9 |
10 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2 |
10 infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2 addsimps2 delsimps2 |
11 addSss addss addIffs delIffs; |
11 addSss addss addss' addIffs delIffs; |
12 |
12 |
13 signature CLASIMP_DATA = |
13 signature CLASIMP_DATA = |
14 sig |
14 sig |
15 structure Simplifier: SIMPLIFIER |
15 structure Simplifier: SIMPLIFIER |
16 structure Splitter: SPLITTER |
16 structure Splitter: SPLITTER |
38 val addDs2: clasimpset * thm list -> clasimpset |
38 val addDs2: clasimpset * thm list -> clasimpset |
39 val addsimps2: clasimpset * thm list -> clasimpset |
39 val addsimps2: clasimpset * thm list -> clasimpset |
40 val delsimps2: clasimpset * thm list -> clasimpset |
40 val delsimps2: clasimpset * thm list -> clasimpset |
41 val addSss: claset * simpset -> claset |
41 val addSss: claset * simpset -> claset |
42 val addss: claset * simpset -> claset |
42 val addss: claset * simpset -> claset |
|
43 val addss': claset * simpset -> claset |
43 val addIffs: clasimpset * thm list -> clasimpset |
44 val addIffs: clasimpset * thm list -> clasimpset |
44 val delIffs: clasimpset * thm list -> clasimpset |
45 val delIffs: clasimpset * thm list -> clasimpset |
45 val AddIffs: thm list -> unit |
46 val AddIffs: thm list -> unit |
46 val DelIffs: thm list -> unit |
47 val DelIffs: thm list -> unit |
47 val CLASIMPSET: (clasimpset -> tactic) -> tactic |
48 val CLASIMPSET: (clasimpset -> tactic) -> tactic |
108 (*Caution: only one simpset added can be added by each of addSss and addss*) |
109 (*Caution: only one simpset added can be added by each of addSss and addss*) |
109 fun cs addSss ss = Classical.addSafter (cs, ("safe_asm_full_simp_tac", |
110 fun cs addSss ss = Classical.addSafter (cs, ("safe_asm_full_simp_tac", |
110 CHANGED o safe_asm_full_simp_tac ss)); |
111 CHANGED o safe_asm_full_simp_tac ss)); |
111 fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
112 fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
112 CHANGED o Simplifier.asm_full_simp_tac ss)); |
113 CHANGED o Simplifier.asm_full_simp_tac ss)); |
|
114 fun cs addss' ss = Classical.addbefore (cs, ("asm_full_simp_tac", |
|
115 CHANGED o Simplifier.asm_lr_simp_tac ss)); |
113 |
116 |
114 |
117 |
115 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
118 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
116 |
119 |
117 (*Takes (possibly conditional) theorems of the form A<->B to |
120 (*Takes (possibly conditional) theorems of the form A<->B to |