Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fri, 30 Jul 1999 18:27:25 +0200 even more stuff;
changeset
wenzelm [Fri, 30 Jul 1999 18:27:25 +0200] rev 7141
even more stuff;
Fri, 30 Jul 1999 15:59:00 +0200 oracle: '=';
changeset
wenzelm [Fri, 30 Jul 1999 15:59:00 +0200] rev 7140
oracle: '=';
Fri, 30 Jul 1999 15:57:50 +0200 added \text;
changeset
wenzelm [Fri, 30 Jul 1999 15:57:50 +0200] rev 7139
added \text;
Fri, 30 Jul 1999 15:57:27 +0200 Isabelle/Isar macros;
changeset
wenzelm [Fri, 30 Jul 1999 15:57:27 +0200] rev 7138
Isabelle/Isar macros;
Fri, 30 Jul 1999 15:56:58 +0200 hacking the rail package;
changeset
wenzelm [Fri, 30 Jul 1999 15:56:58 +0200] rev 7137
hacking the rail package;
Fri, 30 Jul 1999 15:56:33 +0200 added update_thy_only;
changeset
wenzelm [Fri, 30 Jul 1999 15:56:33 +0200] rev 7136
added update_thy_only; moved update_thy;
Fri, 30 Jul 1999 15:40:54 +0200 more;
changeset
wenzelm [Fri, 30 Jul 1999 15:40:54 +0200] rev 7135
more;
Fri, 30 Jul 1999 14:59:32 +0200 more stuff;
changeset
wenzelm [Fri, 30 Jul 1999 14:59:32 +0200] rev 7134
more stuff;
Fri, 30 Jul 1999 13:44:29 +0200 renamed 'same' to '-';
changeset
wenzelm [Fri, 30 Jul 1999 13:44:29 +0200] rev 7133
renamed 'same' to '-';
Fri, 30 Jul 1999 13:43:26 +0200 eliminated METHOD0 in favour of same_tac;
changeset
wenzelm [Fri, 30 Jul 1999 13:43:26 +0200] rev 7132
eliminated METHOD0 in favour of same_tac;
Fri, 30 Jul 1999 13:42:57 +0200 'arith' proof method;
changeset
wenzelm [Fri, 30 Jul 1999 13:42:57 +0200] rev 7131
'arith' proof method;
Fri, 30 Jul 1999 13:41:43 +0200 added erule;
changeset
wenzelm [Fri, 30 Jul 1999 13:41:43 +0200] rev 7130
added erule; renamed same to -;
Fri, 30 Jul 1999 13:34:27 +0200 export sysify_path;
changeset
wenzelm [Fri, 30 Jul 1999 13:34:27 +0200] rev 7129
export sysify_path;
Fri, 30 Jul 1999 09:37:57 +0200 split_diff and remove_diff_ss
changeset
paulson [Fri, 30 Jul 1999 09:37:57 +0200] rev 7128
split_diff and remove_diff_ss
Thu, 29 Jul 1999 12:44:57 +0200 added parentheses to cope with a possible reduction of the precedence of unary
changeset
paulson [Thu, 29 Jul 1999 12:44:57 +0200] rev 7127
added parentheses to cope with a possible reduction of the precedence of unary minus
Wed, 28 Jul 1999 22:01:58 +0200 ML_HOME=$ISABELLE_HOME/../smlnj/bin;
changeset
wenzelm [Wed, 28 Jul 1999 22:01:58 +0200] rev 7126
ML_HOME=$ISABELLE_HOME/../smlnj/bin;
Wed, 28 Jul 1999 19:14:33 +0200 HOL-Real target now builds an actual image;
changeset
wenzelm [Wed, 28 Jul 1999 19:14:33 +0200] rev 7125
HOL-Real target now builds an actual image;
Wed, 28 Jul 1999 18:55:35 +0200 added pretty_setmargin;
changeset
wenzelm [Wed, 28 Jul 1999 18:55:35 +0200] rev 7124
added pretty_setmargin;
Wed, 28 Jul 1999 13:55:34 +0200 congruence rule for |-, etc.
changeset
paulson [Wed, 28 Jul 1999 13:55:34 +0200] rev 7123
congruence rule for |-, etc.
Wed, 28 Jul 1999 13:55:02 +0200 renamed ...thm_pack... to ...pack...
changeset
paulson [Wed, 28 Jul 1999 13:55:02 +0200] rev 7122
renamed ...thm_pack... to ...pack...
Wed, 28 Jul 1999 13:52:59 +0200 removed the unused SeqVar option
changeset
paulson [Wed, 28 Jul 1999 13:52:59 +0200] rev 7121
removed the unused SeqVar option
Wed, 28 Jul 1999 13:50:35 +0200 sequents require higher bounds
changeset
paulson [Wed, 28 Jul 1999 13:50:35 +0200] rev 7120
sequents require higher bounds
Wed, 28 Jul 1999 13:46:51 +0200 more examples are working
changeset
paulson [Wed, 28 Jul 1999 13:46:51 +0200] rev 7119
more examples are working
Wed, 28 Jul 1999 13:45:54 +0200 adding missing declarations for the <<...>> notation
changeset
paulson [Wed, 28 Jul 1999 13:45:54 +0200] rev 7118
adding missing declarations for the <<...>> notation
Wed, 28 Jul 1999 13:45:33 +0200 congruence rule for |-
changeset
paulson [Wed, 28 Jul 1999 13:45:33 +0200] rev 7117
congruence rule for |-
Wed, 28 Jul 1999 13:42:20 +0200 simplifier and improved classical reasoner
changeset
paulson [Wed, 28 Jul 1999 13:42:20 +0200] rev 7116
simplifier and improved classical reasoner
Wed, 28 Jul 1999 12:07:08 +0200 mkdir contrib;
changeset
wenzelm [Wed, 28 Jul 1999 12:07:08 +0200] rev 7115
mkdir contrib;
Wed, 28 Jul 1999 10:28:34 +0200 added String.concat
changeset
paulson [Wed, 28 Jul 1999 10:28:34 +0200] rev 7114
added String.concat
Wed, 28 Jul 1999 10:28:08 +0200 LK
changeset
paulson [Wed, 28 Jul 1999 10:28:08 +0200] rev 7113
LK
Tue, 27 Jul 1999 22:34:11 +0200 back again, supposedly with correct perms;
changeset
wenzelm [Tue, 27 Jul 1999 22:34:11 +0200] rev 7112
back again, supposedly with correct perms;
Tue, 27 Jul 1999 22:33:27 +0200 *** empty log message ***
changeset
wenzelm [Tue, 27 Jul 1999 22:33:27 +0200] rev 7111
*** empty log message ***
Tue, 27 Jul 1999 22:32:22 +0200 fixed perms and final nl;
changeset
wenzelm [Tue, 27 Jul 1999 22:32:22 +0200] rev 7110
fixed perms and final nl;
Tue, 27 Jul 1999 22:04:54 +0200 fixed comments;
changeset
wenzelm [Tue, 27 Jul 1999 22:04:54 +0200] rev 7109
fixed comments;
Tue, 27 Jul 1999 22:04:30 +0200 fixed comment;
changeset
wenzelm [Tue, 27 Jul 1999 22:04:30 +0200] rev 7108
fixed comment;
Tue, 27 Jul 1999 22:03:24 +0200 inductive_cases(_i): Isar interface to mk_cases;
changeset
wenzelm [Tue, 27 Jul 1999 22:03:24 +0200] rev 7107
inductive_cases(_i): Isar interface to mk_cases;
Tue, 27 Jul 1999 22:00:00 +0200 safe_step_tac / step_tac;
changeset
wenzelm [Tue, 27 Jul 1999 22:00:00 +0200] rev 7106
safe_step_tac / step_tac;
Tue, 27 Jul 1999 21:59:23 +0200 init / init_theory: pass int flag;
changeset
wenzelm [Tue, 27 Jul 1999 21:59:23 +0200] rev 7105
init / init_theory: pass int flag;
Tue, 27 Jul 1999 21:58:59 +0200 added thy_switch kind;
changeset
wenzelm [Tue, 27 Jul 1999 21:58:59 +0200] rev 7104
added thy_switch kind;
Tue, 27 Jul 1999 21:58:39 +0200 removed update_context;
changeset
wenzelm [Tue, 27 Jul 1999 21:58:39 +0200] rev 7103
removed update_context; context / theory: proper update in interactive mode;
Tue, 27 Jul 1999 21:57:58 +0200 removed update_context;
changeset
wenzelm [Tue, 27 Jul 1999 21:57:58 +0200] rev 7102
removed update_context; removed restart; added init_toplevel, touch_all_thys, touch_thy, remove_thy, update_thy_only;
Tue, 27 Jul 1999 21:56:32 +0200 removed restart;
changeset
wenzelm [Tue, 27 Jul 1999 21:56:32 +0200] rev 7101
removed restart; added touch_all_thys, touch_thy, remove_thy, update_thy_only;
Tue, 27 Jul 1999 21:55:39 +0200 setup_thy_loader;
changeset
wenzelm [Tue, 27 Jul 1999 21:55:39 +0200] rev 7100
setup_thy_loader;
Tue, 27 Jul 1999 21:55:19 +0200 added update_thy_only;
changeset
wenzelm [Tue, 27 Jul 1999 21:55:19 +0200] rev 7099
added update_thy_only; added theory loader action hook; added touch_all_thys; touch_thy: all_succs;
Tue, 27 Jul 1999 19:02:43 +0200 installation of simplifier and classical reasoner, better rules etc
changeset
paulson [Tue, 27 Jul 1999 19:02:43 +0200] rev 7098
installation of simplifier and classical reasoner, better rules etc
Tue, 27 Jul 1999 19:01:46 +0200 moved the modal prover to modal.ML; installed the prover using TheoryDataFun
changeset
paulson [Tue, 27 Jul 1999 19:01:46 +0200] rev 7097
moved the modal prover to modal.ML; installed the prover using TheoryDataFun
Tue, 27 Jul 1999 19:00:55 +0200 split off modal.ML from provers.ML
changeset
paulson [Tue, 27 Jul 1999 19:00:55 +0200] rev 7096
split off modal.ML from provers.ML
Tue, 27 Jul 1999 18:58:40 +0200 fixed the comments...
changeset
paulson [Tue, 27 Jul 1999 18:58:40 +0200] rev 7095
fixed the comments...
Tue, 27 Jul 1999 18:52:48 +0200 a new theory containing just an axiom needed to derive imp_cong
changeset
paulson [Tue, 27 Jul 1999 18:52:48 +0200] rev 7094
a new theory containing just an axiom needed to derive imp_cong
Tue, 27 Jul 1999 18:52:23 +0200 renamed theory LK to LK0
changeset
paulson [Tue, 27 Jul 1999 18:52:23 +0200] rev 7093
renamed theory LK to LK0
Tue, 27 Jul 1999 18:52:08 +0200 renamed LK0.ML
changeset
paulson [Tue, 27 Jul 1999 18:52:08 +0200] rev 7092
renamed LK0.ML
Tue, 27 Jul 1999 18:50:14 +0200 Sequents/LK/Nat: new example of simplification in LK
changeset
paulson [Tue, 27 Jul 1999 18:50:14 +0200] rev 7091
Sequents/LK/Nat: new example of simplification in LK
Tue, 27 Jul 1999 17:30:25 +0200 added gen_inter
changeset
paulson [Tue, 27 Jul 1999 17:30:25 +0200] rev 7090
added gen_inter
Tue, 27 Jul 1999 17:19:31 +0200 expandshort and tidying
changeset
paulson [Tue, 27 Jul 1999 17:19:31 +0200] rev 7089
expandshort and tidying
Tue, 27 Jul 1999 10:30:26 +0200 expandshort; tidied
changeset
paulson [Tue, 27 Jul 1999 10:30:26 +0200] rev 7088
expandshort; tidied
Tue, 27 Jul 1999 10:29:46 +0200 tidied
changeset
paulson [Tue, 27 Jul 1999 10:29:46 +0200] rev 7087
tidied
Mon, 26 Jul 1999 16:32:23 +0200 expandshort
changeset
paulson [Mon, 26 Jul 1999 16:32:23 +0200] rev 7086
expandshort
(0) -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle