46 val fix: (binding * string option * mixfix) list -> state -> state |
46 val fix: (binding * string option * mixfix) list -> state -> state |
47 val fix_i: (binding * typ option * mixfix) list -> state -> state |
47 val fix_i: (binding * typ option * mixfix) list -> state -> state |
48 val assm: Assumption.export -> |
48 val assm: Assumption.export -> |
49 (Attrib.binding * (string * string list) list) list -> state -> state |
49 (Attrib.binding * (string * string list) list) list -> state -> state |
50 val assm_i: Assumption.export -> |
50 val assm_i: Assumption.export -> |
51 ((binding * attribute list) * (term * term list) list) list -> state -> state |
51 (Thm.binding * (term * term list) list) list -> state -> state |
52 val assume: (Attrib.binding * (string * string list) list) list -> state -> state |
52 val assume: (Attrib.binding * (string * string list) list) list -> state -> state |
53 val assume_i: ((binding * attribute list) * (term * term list) list) list -> |
53 val assume_i: (Thm.binding * (term * term list) list) list -> state -> state |
54 state -> state |
|
55 val presume: (Attrib.binding * (string * string list) list) list -> state -> state |
54 val presume: (Attrib.binding * (string * string list) list) list -> state -> state |
56 val presume_i: ((binding * attribute list) * (term * term list) list) list -> |
55 val presume_i: (Thm.binding * (term * term list) list) list -> state -> state |
57 state -> state |
56 val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state |
58 val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> |
57 val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state |
59 state -> state |
|
60 val def_i: ((binding * attribute list) * |
|
61 ((binding * mixfix) * (term * term list))) list -> state -> state |
|
62 val chain: state -> state |
58 val chain: state -> state |
63 val chain_facts: thm list -> state -> state |
59 val chain_facts: thm list -> state -> state |
64 val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list |
60 val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list |
65 val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state |
61 val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state |
66 val note_thmss_i: ((binding * attribute list) * |
62 val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state |
67 (thm list * attribute list) list) list -> state -> state |
|
68 val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state |
63 val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state |
69 val from_thmss_i: ((thm list * attribute list) list) list -> state -> state |
64 val from_thmss_i: ((thm list * attribute list) list) list -> state -> state |
70 val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state |
65 val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state |
71 val with_thmss_i: ((thm list * attribute list) list) list -> state -> state |
66 val with_thmss_i: ((thm list * attribute list) list) list -> state -> state |
72 val using: ((Facts.ref * Attrib.src list) list) list -> state -> state |
67 val using: ((Facts.ref * Attrib.src list) list) list -> state -> state |
105 val global_skip_proof: bool -> state -> context |
100 val global_skip_proof: bool -> state -> context |
106 val global_done_proof: state -> context |
101 val global_done_proof: state -> context |
107 val have: Method.text option -> (thm list list -> state -> state) -> |
102 val have: Method.text option -> (thm list list -> state -> state) -> |
108 (Attrib.binding * (string * string list) list) list -> bool -> state -> state |
103 (Attrib.binding * (string * string list) list) list -> bool -> state -> state |
109 val have_i: Method.text option -> (thm list list -> state -> state) -> |
104 val have_i: Method.text option -> (thm list list -> state -> state) -> |
110 ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state |
105 (Thm.binding * (term * term list) list) list -> bool -> state -> state |
111 val show: Method.text option -> (thm list list -> state -> state) -> |
106 val show: Method.text option -> (thm list list -> state -> state) -> |
112 (Attrib.binding * (string * string list) list) list -> bool -> state -> state |
107 (Attrib.binding * (string * string list) list) list -> bool -> state -> state |
113 val show_i: Method.text option -> (thm list list -> state -> state) -> |
108 val show_i: Method.text option -> (thm list list -> state -> state) -> |
114 ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state |
109 (Thm.binding * (term * term list) list) list -> bool -> state -> state |
115 val schematic_goal: state -> bool |
110 val schematic_goal: state -> bool |
116 val is_relevant: state -> bool |
111 val is_relevant: state -> bool |
117 val local_future_proof: (state -> ('a * state) Future.future) -> |
112 val local_future_proof: (state -> ('a * state) Future.future) -> |
118 state -> 'a Future.future * state |
113 state -> 'a Future.future * state |
119 val global_future_proof: (state -> ('a * Proof.context) Future.future) -> |
114 val global_future_proof: (state -> ('a * Proof.context) Future.future) -> |