9 |
9 |
10 infix 4 addsplits delsplits; |
10 infix 4 addsplits delsplits; |
11 |
11 |
12 signature SPLITTER_DATA = |
12 signature SPLITTER_DATA = |
13 sig |
13 sig |
|
14 val thy : theory |
14 val mk_eq : thm -> thm |
15 val mk_eq : thm -> thm |
15 val meta_eq_to_iff: thm (* "x == y ==> x = y" *) |
16 val meta_eq_to_iff: thm (* "x == y ==> x = y" *) |
16 val iffD : thm (* "[| P = Q; Q |] ==> P" *) |
17 val iffD : thm (* "[| P = Q; Q |] ==> P" *) |
17 val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *) |
18 val disjE : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *) |
18 val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *) |
19 val conjE : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *) |
38 val split_del: attribute |
39 val split_del: attribute |
39 val split_modifiers : Method.modifier parser list |
40 val split_modifiers : Method.modifier parser list |
40 val setup: theory -> theory |
41 val setup: theory -> theory |
41 end; |
42 end; |
42 |
43 |
43 functor SplitterFun(Data: SPLITTER_DATA): SPLITTER = |
44 functor Splitter(Data: SPLITTER_DATA): SPLITTER = |
44 struct |
45 struct |
45 |
46 |
46 val Const (const_not, _) $ _ = |
47 val Const (const_not, _) $ _ = |
47 ObjectLogic.drop_judgment (OldGoals.the_context ()) |
48 ObjectLogic.drop_judgment Data.thy |
48 (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD))); |
49 (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD))); |
49 |
50 |
50 val Const (const_or , _) $ _ $ _ = |
51 val Const (const_or , _) $ _ $ _ = |
51 ObjectLogic.drop_judgment (OldGoals.the_context ()) |
52 ObjectLogic.drop_judgment Data.thy |
52 (#1 (Logic.dest_implies (Thm.prop_of Data.disjE))); |
53 (#1 (Logic.dest_implies (Thm.prop_of Data.disjE))); |
53 |
54 |
54 val const_Trueprop = ObjectLogic.judgment_name (OldGoals.the_context ()); |
55 val const_Trueprop = ObjectLogic.judgment_name Data.thy; |
55 |
56 |
56 |
57 |
57 fun split_format_err () = error "Wrong format for split rule"; |
58 fun split_format_err () = error "Wrong format for split rule"; |
58 |
59 |
59 (* thm -> (string * typ) * bool *) |
60 (* thm -> (string * typ) * bool *) |