| #
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap;
tuned comments;
|
| #
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
| #
d70d74b6 |
|
05-Apr-2016 |
wenzelm <none@none> |
clarified modules -- simplified bootstrap;
|
| #
e3afad2b |
|
28-Jul-2015 |
wenzelm <none@none> |
more explicit context;
tuned signature;
|
| #
56064dd0 |
|
28-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
| #
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
| #
94a128ac |
|
01-Jul-2015 |
wenzelm <none@none> |
support for subgoal focus command;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
92c442b3 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
| #
0d27b506 |
|
15-Feb-2012 |
wenzelm <none@none> |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
| #
b6f9ad57 |
|
09-Jun-2011 |
wenzelm <none@none> |
tuned signature: Name.invent and Name.invent_names;
|
| #
330ecb2e |
|
27-Mar-2010 |
wenzelm <none@none> |
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def;
modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
|
| #
bbc8cf56 |
|
20-Mar-2010 |
wenzelm <none@none> |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
| #
c9975fc3 |
|
02-Nov-2009 |
wenzelm <none@none> |
modernized structure Simple_Syntax;
|
| #
5fe60907 |
|
28-Oct-2009 |
wenzelm <none@none> |
Drule.store: proper binding;
conceal internal bindings;
|
| #
8518a24a |
|
29-Sep-2009 |
wenzelm <none@none> |
modernized Balanced_Tree;
|
| #
2111d86f |
|
31-Mar-2009 |
wenzelm <none@none> |
added dest_conjunctions (cf. Logic.dest_conjunctions);
|
| #
1bd59ac7 |
|
21-Jan-2009 |
wenzelm <none@none> |
removed Ids;
|
| #
b08c2db5 |
|
19-Nov-2008 |
wenzelm <none@none> |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
| #
4e5786a4 |
|
23-Oct-2008 |
wenzelm <none@none> |
renamed Thm.get_axiom_i to Thm.axiom;
|
| #
d4aa0c76 |
|
15-Apr-2008 |
wenzelm <none@none> |
Thm.forall_elim_var(s);
|
| #
292ed3a3 |
|
29-Mar-2008 |
wenzelm <none@none> |
certify wrt. dynamic context;
|
| #
a6067101 |
|
27-Mar-2008 |
wenzelm <none@none> |
eliminated theory ProtoPure;
|
| #
a2a15bc0 |
|
11-Oct-2007 |
wenzelm <none@none> |
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
|
| #
64072809 |
|
13-Aug-2007 |
wenzelm <none@none> |
SimpleSyntax.read_prop;
|
| #
94711cf4 |
|
03-Jul-2007 |
wenzelm <none@none> |
removed obsolete mk_conjunction_list, intr/elim_list;
|
| #
d5f5607c |
|
19-Jun-2007 |
wenzelm <none@none> |
balanced conjunctions;
tuned interfaces;
tuned;
|
| #
89015704 |
|
27-Nov-2006 |
wenzelm <none@none> |
simplified '?' operator;
|
| #
7937260e |
|
21-Sep-2006 |
wenzelm <none@none> |
Thm.dest_binop;
|
| #
8a6aa5f8 |
|
11-Sep-2006 |
wenzelm <none@none> |
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
|
| #
3f949d55 |
|
30-Jul-2006 |
wenzelm <none@none> |
Thm.adjust_maxidx;
|
| #
e9c864be |
|
28-Jul-2006 |
wenzelm <none@none> |
added mk_conjunction_list;
|
| #
75d0d35e |
|
27-Jul-2006 |
wenzelm <none@none> |
eliminated obsolete freeze_thaw;
|
| #
ebb30c8e |
|
12-Apr-2006 |
wenzelm <none@none> |
Meta-level conjunction.
|