Sun, 13 Jan 2002 21:14:51 +0100 |
wenzelm |
\<twosuperior> syntax moved to HOL/Numerals;
|
changeset |
files
|
Sun, 13 Jan 2002 21:14:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sun, 13 Jan 2002 21:14:14 +0100 |
wenzelm |
prime_dvd_power_two;
|
changeset |
files
|
Sun, 13 Jan 2002 21:13:59 +0100 |
wenzelm |
symbolic syntax for x^2 (faills back on plain infix "^");
|
changeset |
files
|
Sun, 13 Jan 2002 21:13:27 +0100 |
wenzelm |
\usepackage[latin1]{inputenc};
|
changeset |
files
|
Sun, 13 Jan 2002 21:12:43 +0100 |
wenzelm |
* HOL: symbolic syntax for x^2 (numeral 2);
|
changeset |
files
|
Sun, 13 Jan 2002 21:09:17 +0100 |
wenzelm |
added HOL/Real/document/root.tex;
|
changeset |
files
|
Sun, 13 Jan 2002 19:45:17 +0100 |
wenzelm |
HOL-Real/Complex_Numbers;
|
changeset |
files
|
Sun, 13 Jan 2002 19:42:30 +0100 |
wenzelm |
Real/Complex_Numbers.thy;
|
changeset |
files
|
Sat, 12 Jan 2002 22:44:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 12 Jan 2002 22:24:09 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 12 Jan 2002 22:17:08 +0100 |
wenzelm |
produce predicate text;
|
changeset |
files
|
Sat, 12 Jan 2002 22:15:48 +0100 |
wenzelm |
added atomize_cterm;
|
changeset |
files
|
Sat, 12 Jan 2002 16:55:53 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 12 Jan 2002 16:40:02 +0100 |
wenzelm |
unify_frozen: proper use of maxidx';
|
changeset |
files
|
Sat, 12 Jan 2002 16:38:42 +0100 |
wenzelm |
paramify_dummies: proper treatment of maxidx;
|
changeset |
files
|
Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
changeset |
files
|
Fri, 11 Jan 2002 18:49:25 +0100 |
wenzelm |
Isabelle2002 (January 2002);
|
changeset |
files
|
Fri, 11 Jan 2002 18:07:45 +0100 |
wenzelm |
removed obsolete isamode.ML;
|
changeset |
files
|
Fri, 11 Jan 2002 18:07:30 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 11 Jan 2002 17:04:49 +0100 |
wenzelm |
#!/usr/bin/env bash;
|
changeset |
files
|
Fri, 11 Jan 2002 14:53:30 +0100 |
wenzelm |
replace gen_all by forall_elim_vars_safe;
|
changeset |
files
|
Fri, 11 Jan 2002 14:53:05 +0100 |
wenzelm |
improved forall_elim_vars_safe (no longer invents new indexes);
|
changeset |
files
|
Fri, 11 Jan 2002 14:44:58 +0100 |
wenzelm |
lemmas (in ACe) AC;
|
changeset |
files
|
Fri, 11 Jan 2002 14:44:24 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 11 Jan 2002 00:35:03 +0100 |
wenzelm |
IsarThy.theorems_i;
|
changeset |
files
|
Fri, 11 Jan 2002 00:34:43 +0100 |
wenzelm |
moved setmksimps to Main!
|
changeset |
files
|
Fri, 11 Jan 2002 00:33:35 +0100 |
wenzelm |
have_thmss vs. have_thmss_i;
|
changeset |
files
|
Fri, 11 Jan 2002 00:32:17 +0100 |
wenzelm |
clarified/added theorems(_i) vs. locale_theorems(_i);
|
changeset |
files
|
Fri, 11 Jan 2002 00:30:28 +0100 |
wenzelm |
localized 'lemmas', 'theorems', 'declare';
|
changeset |
files
|
Fri, 11 Jan 2002 00:29:54 +0100 |
wenzelm |
have_thmss vs. have_thmss_i;
|
changeset |
files
|
Fri, 11 Jan 2002 00:29:25 +0100 |
wenzelm |
kind: ignore "";
|
changeset |
files
|
Fri, 11 Jan 2002 00:28:43 +0100 |
wenzelm |
IsarThy.theorems_i;
|
changeset |
files
|
Fri, 11 Jan 2002 00:28:24 +0100 |
wenzelm |
clarified IsarThy.apply_theorems_i;
|
changeset |
files
|
Fri, 11 Jan 2002 00:27:40 +0100 |
wenzelm |
* Pure: localized 'lemmas', 'theorems', 'declare';
|
changeset |
files
|
Thu, 10 Jan 2002 21:04:15 +0100 |
wenzelm |
removed add_thmss;
|
changeset |
files
|
Thu, 10 Jan 2002 21:03:46 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 10 Jan 2002 16:09:26 +0100 |
wenzelm |
export_single;
|
changeset |
files
|
Thu, 10 Jan 2002 16:06:39 +0100 |
wenzelm |
refine_tac: Tactic.norm_hhf_tac before trying rule;
|
changeset |
files
|
Thu, 10 Jan 2002 16:04:42 +0100 |
wenzelm |
add_thmss_hybrid;
|
changeset |
files
|
Thu, 10 Jan 2002 16:04:28 +0100 |
wenzelm |
export multi_theorem(_i), locale_multi_theorem(_i);
|
changeset |
files
|
Thu, 10 Jan 2002 13:25:48 +0100 |
paulson |
stylistic changes
|
changeset |
files
|
Thu, 10 Jan 2002 11:22:03 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Thu, 10 Jan 2002 01:13:41 +0100 |
wenzelm |
locales: hide base name of exported version;
|
changeset |
files
|
Thu, 10 Jan 2002 01:13:07 +0100 |
wenzelm |
simplified theorem(_i);
|
changeset |
files
|
Thu, 10 Jan 2002 01:12:30 +0100 |
wenzelm |
IsarThy.smart_multi_theorem;
|
changeset |
files
|
Thu, 10 Jan 2002 01:12:01 +0100 |
wenzelm |
added hide_thms;
|
changeset |
files
|
Thu, 10 Jan 2002 01:11:43 +0100 |
wenzelm |
simplified IsarThy.theorem_i;
|
changeset |
files
|
Thu, 10 Jan 2002 01:10:58 +0100 |
wenzelm |
qualified exports from locales;
|
changeset |
files
|
Wed, 09 Jan 2002 17:56:46 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
Wed, 09 Jan 2002 17:48:40 +0100 |
wenzelm |
converted theory Transitive_Closure;
|
changeset |
files
|
Wed, 09 Jan 2002 17:42:49 +0100 |
wenzelm |
* added \<euro> symbol;
|
changeset |
files
|
Wed, 09 Jan 2002 17:36:54 +0100 |
wenzelm |
no longer requires TEXINPUTS;
|
changeset |
files
|
Wed, 09 Jan 2002 17:36:34 +0100 |
wenzelm |
isatool latex -o sty;
|
changeset |
files
|
Wed, 09 Jan 2002 17:36:18 +0100 |
wenzelm |
removed TEXINPUTS;
|
changeset |
files
|
Wed, 09 Jan 2002 14:44:24 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Wed, 09 Jan 2002 14:44:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 09 Jan 2002 14:25:22 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Wed, 09 Jan 2002 14:25:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 09 Jan 2002 14:01:13 +0100 |
wenzelm |
updated;
|
changeset |
files
|