2002-01-10 |
wenzelm |
have_thmss vs. have_thmss_i;
|
file |
diff |
annotate
|
2002-01-10 |
wenzelm |
added hide_thms;
|
file |
diff |
annotate
|
2001-11-27 |
wenzelm |
theory data: removed obsolete finish method;
|
file |
diff |
annotate
|
2001-11-20 |
wenzelm |
trfuns *after* binder syntax;
|
file |
diff |
annotate
|
2001-11-19 |
berghofe |
Further restructuring of theorem naming functions.
|
file |
diff |
annotate
|
2001-11-11 |
wenzelm |
renamed open_smart_store_thms to smart_store_thms_open;
|
file |
diff |
annotate
|
2001-11-08 |
wenzelm |
theory data: finish method;
|
file |
diff |
annotate
|
2001-10-31 |
berghofe |
- enter_thmx -> enter_thms
|
file |
diff |
annotate
|
2001-09-28 |
wenzelm |
internal thm numbering with ":" instead of "_";
|
file |
diff |
annotate
|
2001-08-31 |
berghofe |
Added equality axioms and initialization of proof term package.
|
file |
diff |
annotate
|
2000-12-13 |
wenzelm |
eliminated GOAL syntax;
|
file |
diff |
annotate
|
2000-11-12 |
wenzelm |
Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
|
file |
diff |
annotate
|
2000-09-17 |
wenzelm |
Display.pretty_thm_sg;
|
file |
diff |
annotate
|
2000-09-02 |
wenzelm |
added get_thm_closure;
|
file |
diff |
annotate
|
2000-08-09 |
wenzelm |
added get_thms_closure, single_thm;
|
file |
diff |
annotate
|
2000-08-04 |
wenzelm |
dummy_pattern moved to term.ML;
|
file |
diff |
annotate
|
2000-07-13 |
wenzelm |
add_defs(_i): overloaded option;
|
file |
diff |
annotate
|
2000-07-03 |
wenzelm |
added "nothing" (empty list of theorems);
|
file |
diff |
annotate
|
2000-07-01 |
wenzelm |
print_theorems: omit name space;
|
file |
diff |
annotate
|
2000-06-29 |
wenzelm |
have_thmss: handle multiple lists of arguments;
|
file |
diff |
annotate
|
2000-05-31 |
wenzelm |
get_thm(s): automatic transfer;
|
file |
diff |
annotate
|
2000-04-17 |
wenzelm |
Pretty.chunks;
|
file |
diff |
annotate
|
2000-03-13 |
wenzelm |
add_thms, add_axioms, add_defs: return theorems as well;
|
file |
diff |
annotate
|
1999-11-29 |
wenzelm |
Goal: tuned pris;
|
file |
diff |
annotate
|
1999-10-27 |
wenzelm |
dummy_pattern: aprop;
|
file |
diff |
annotate
|
1999-10-21 |
wenzelm |
forall_elim_var(s) move here from drule.ML;
|
file |
diff |
annotate
|
1999-10-08 |
wenzelm |
theorem database now also indexes constants "Trueprop", "all",
|
file |
diff |
annotate
|
1999-10-06 |
wenzelm |
fixed naming of single axioms;
|
file |
diff |
annotate
|
1999-09-06 |
wenzelm |
removed thms_closure (unused);
|
file |
diff |
annotate
|
1999-09-04 |
wenzelm |
eliminated default_name (thms no longer stored for name "");
|
file |
diff |
annotate
|