nipkow [Tue, 17 Apr 2001 19:28:04 +0200] rev 11257
*** empty log message ***
nipkow [Tue, 17 Apr 2001 16:54:38 +0200] rev 11256
*** empty log message ***
paulson [Tue, 17 Apr 2001 15:03:41 +0200] rev 11255
*** empty log message ***
wenzelm [Mon, 16 Apr 2001 15:34:33 +0200] rev 11254
TODO
wenzelm [Thu, 12 Apr 2001 18:05:41 +0200] rev 11253
proper order of order_less_asym';
kleing [Thu, 12 Apr 2001 13:40:15 +0200] rev 11252
cleanup, tuned
paulson [Thu, 12 Apr 2001 12:45:05 +0200] rev 11251
converted many HOL/Auth theories to Isar scripts
paulson [Wed, 11 Apr 2001 11:53:54 +0200] rev 11250
symlinks to ../../../HOL/Auth. Fingers crossed...
paulson [Tue, 10 Apr 2001 16:11:01 +0200] rev 11249
Protocols chapter
paulson [Tue, 10 Apr 2001 16:09:26 +0200] rev 11248
back to Unix format...
paulson [Tue, 10 Apr 2001 16:02:01 +0200] rev 11247
security protocol chapter
paulson [Tue, 10 Apr 2001 15:58:50 +0200] rev 11246
security protocol refs
paulson [Mon, 09 Apr 2001 14:49:51 +0200] rev 11245
new theorem Fake_parts_insert_in_Un
paulson [Mon, 09 Apr 2001 10:12:33 +0200] rev 11244
extra display
paulson [Mon, 09 Apr 2001 10:12:12 +0200] rev 11243
*** empty log message ***
paulson [Mon, 09 Apr 2001 10:11:59 +0200] rev 11242
lexicographic product of two relations: updated HOL.tex
Also automatic updates by xemacs
paulson [Mon, 09 Apr 2001 10:10:21 +0200] rev 11241
Isar hint
wenzelm [Sat, 07 Apr 2001 19:38:50 +0200] rev 11240
thm output: Attrib.local_thmss;
wenzelm [Sat, 07 Apr 2001 19:38:01 +0200] rev 11239
tuned
nipkow [Fri, 30 Mar 2001 18:35:33 +0200] rev 11238
*** empty log message ***
nipkow [Fri, 30 Mar 2001 18:18:22 +0200] rev 11237
*** empty log message ***
nipkow [Fri, 30 Mar 2001 18:12:26 +0200] rev 11236
*** empty log message ***
nipkow [Fri, 30 Mar 2001 16:12:57 +0200] rev 11235
*** empty log message ***
paulson [Fri, 30 Mar 2001 13:29:16 +0200] rev 11234
quantifier instantiation
paulson [Fri, 30 Mar 2001 12:31:10 +0200] rev 11233
the one-point rule for bounded quantifiers
nipkow [Thu, 29 Mar 2001 13:59:54 +0200] rev 11232
generalization of 1 point rules for ALL
nipkow [Thu, 29 Mar 2001 12:26:37 +0200] rev 11231
*** empty log message ***
paulson [Thu, 29 Mar 2001 10:44:37 +0200] rev 11230
misc tidying; changing the predicate isSymKey to the set symKeys
nipkow [Wed, 28 Mar 2001 13:40:06 +0200] rev 11229
Got rid of is_dfa
nipkow [Wed, 28 Mar 2001 13:39:50 +0200] rev 11228
MicroJava/BV dependencies incomplete
nipkow [Tue, 27 Mar 2001 13:00:30 +0200] rev 11227
fixed bug in tactic for ball 1 point simproc
paulson [Tue, 27 Mar 2001 11:27:06 +0200] rev 11226
Vos
nipkow [Mon, 26 Mar 2001 19:37:31 +0200] rev 11225
simplified proofs
nipkow [Mon, 26 Mar 2001 16:31:38 +0200] rev 11224
simplified proofs
nipkow [Mon, 26 Mar 2001 12:51:14 +0200] rev 11223
I forgot a few bases cases for the 1-point rules...
paulson [Fri, 23 Mar 2001 12:10:05 +0100] rev 11222
shortening and streamlining of proofs
nipkow [Fri, 23 Mar 2001 10:12:12 +0100] rev 11221
added simproc for bounded quantifiers
nipkow [Fri, 23 Mar 2001 10:10:53 +0100] rev 11220
added one point simprocs for bounded quantifiers
paulson [Thu, 22 Mar 2001 10:29:26 +0100] rev 11219
new theorem analz_Decrypt'
paulson [Thu, 22 Mar 2001 10:28:46 +0100] rev 11218
new theorem analz_isSymKey_Decrypt
paulson [Thu, 22 Mar 2001 10:27:00 +0100] rev 11217
some X-symbols
nipkow [Mon, 19 Mar 2001 17:25:42 +0100] rev 11216
*** empty log message ***
nipkow [Mon, 19 Mar 2001 13:28:06 +0100] rev 11215
*** empty log message ***
nipkow [Mon, 19 Mar 2001 13:05:56 +0100] rev 11214
*** empty log message ***
nipkow [Mon, 19 Mar 2001 12:38:36 +0100] rev 11213
*** empty log message ***
paulson [Mon, 19 Mar 2001 10:37:47 +0100] rev 11212
*** empty log message ***
paulson [Thu, 15 Mar 2001 16:56:35 +0100] rev 11211
translations: a tweak
nipkow [Thu, 15 Mar 2001 15:05:51 +0100] rev 11210
*** empty log message ***
nipkow [Thu, 15 Mar 2001 13:57:10 +0100] rev 11209
*** empty log message ***
nipkow [Thu, 15 Mar 2001 11:06:33 +0100] rev 11208
*** empty log message ***
nipkow [Thu, 15 Mar 2001 10:41:32 +0100] rev 11207
*** empty log message ***
nipkow [Wed, 14 Mar 2001 18:40:01 +0100] rev 11206
*** empty log message ***
nipkow [Wed, 14 Mar 2001 17:38:49 +0100] rev 11205
*** empty log message ***
paulson [Wed, 14 Mar 2001 08:50:55 +0100] rev 11204
minor tuning
nipkow [Tue, 13 Mar 2001 18:35:48 +0100] rev 11203
*** empty log message ***
nipkow [Mon, 12 Mar 2001 18:23:11 +0100] rev 11202
*** empty log message ***
nipkow [Mon, 12 Mar 2001 18:17:45 +0100] rev 11201
*** empty log message ***
nipkow [Fri, 09 Mar 2001 19:05:48 +0100] rev 11200
arith_tac now copes with propositional reasoning as well.
paulson [Wed, 07 Mar 2001 18:35:27 +0100] rev 11199
expanded abbrevs
streckem [Wed, 07 Mar 2001 17:19:16 +0100] rev 11198
added strange 'b y' syntax
nipkow [Wed, 07 Mar 2001 16:25:51 +0100] rev 11197
*** empty log message ***
nipkow [Wed, 07 Mar 2001 15:54:11 +0100] rev 11196
*** empty log message ***
paulson [Mon, 05 Mar 2001 15:47:11 +0100] rev 11195
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson [Mon, 05 Mar 2001 15:32:54 +0100] rev 11194
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson [Mon, 05 Mar 2001 15:25:11 +0100] rev 11193
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson [Mon, 05 Mar 2001 12:31:31 +0100] rev 11192
a few basic X-symbols
paulson [Fri, 02 Mar 2001 13:26:55 +0100] rev 11191
conversion of Message.thy to Isar format
ehmety [Fri, 02 Mar 2001 13:18:56 +0100] rev 11190
*** empty log message ***
paulson [Fri, 02 Mar 2001 13:18:31 +0100] rev 11189
conversion of Message.thy to Isar format
paulson [Fri, 02 Mar 2001 13:14:37 +0100] rev 11188
streamlined a proof
paulson [Wed, 28 Feb 2001 12:37:48 +0100] rev 11187
auto-update
nipkow [Tue, 27 Feb 2001 23:25:47 +0100] rev 11186
*** empty log message ***
paulson [Tue, 27 Feb 2001 16:13:23 +0100] rev 11185
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Streamlining of Yahalom proofs
Removal of redundant proofs
nipkow [Tue, 27 Feb 2001 12:28:42 +0100] rev 11184
kildall now via while and therefore executable!
paulson [Mon, 26 Feb 2001 16:36:53 +0100] rev 11183
minor tweaks to speed the proofs
paulson [Mon, 26 Feb 2001 10:41:24 +0100] rev 11182
minor fixes
oheimb [Fri, 23 Feb 2001 16:31:21 +0100] rev 11181
renamed addaltern to addafter, addSaltern to addSafter
oheimb [Fri, 23 Feb 2001 16:31:18 +0100] rev 11180
removed performance leak for split_conv_tac (and corresponding safe wrapper)
paulson [Thu, 22 Feb 2001 18:13:23 +0100] rev 11179
subst method and a new section on rule, rule_tac, etc
kleing [Thu, 22 Feb 2001 18:03:11 +0100] rev 11178
removed unused constant
kleing [Thu, 22 Feb 2001 11:47:35 +0100] rev 11177
removed unused function
paulson [Thu, 22 Feb 2001 11:31:31 +0100] rev 11176
a PROPER tidy-up
nipkow [Thu, 22 Feb 2001 10:18:41 +0100] rev 11175
recoded function iter with the help of the while-combinator.
paulson [Wed, 21 Feb 2001 15:21:15 +0100] rev 11174
revisions in response to comments by Tobias
paulson [Wed, 21 Feb 2001 12:57:55 +0100] rev 11173
revisions in response to comments by Tobias
oheimb [Wed, 21 Feb 2001 12:07:00 +0100] rev 11172
added split_conv_tac (also to claset()) as an optimization
oheimb [Tue, 20 Feb 2001 18:53:28 +0100] rev 11171
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
oheimb [Tue, 20 Feb 2001 18:48:34 +0100] rev 11170
simplified proofs for splitI and splitD, added splitD'
added split_conv_tac (also to claset()) as an optimization
made split_all_tac safe introducing safe_full_simp_tac,EXISTING PROOFS MAY FAIL
oheimb [Tue, 20 Feb 2001 18:47:34 +0100] rev 11169
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
oheimb [Tue, 20 Feb 2001 18:47:32 +0100] rev 11168
corrected comments on addbefore and addSbefore
oheimb [Tue, 20 Feb 2001 18:47:30 +0100] rev 11167
added same_fstI
oheimb [Tue, 20 Feb 2001 18:47:29 +0100] rev 11166
simplified definition of wrapper bspec
oheimb [Tue, 20 Feb 2001 18:47:27 +0100] rev 11165
added image_cong to default congs of recdef
oheimb [Tue, 20 Feb 2001 18:47:25 +0100] rev 11164
added add_arith (just as hint by now)
oheimb [Tue, 20 Feb 2001 18:47:22 +0100] rev 11163
added rearrange_prems
oheimb [Tue, 20 Feb 2001 18:47:06 +0100] rev 11162
debugging: replaced gen_all by forall_elim_vars_safe
nipkow [Tue, 20 Feb 2001 13:23:58 +0100] rev 11161
*** empty log message ***
nipkow [Tue, 20 Feb 2001 11:27:04 +0100] rev 11160
*** empty log message ***
nipkow [Tue, 20 Feb 2001 10:37:12 +0100] rev 11159
*** empty log message ***
nipkow [Tue, 20 Feb 2001 10:18:26 +0100] rev 11158
*** empty log message ***
nipkow [Sat, 17 Feb 2001 10:43:53 +0100] rev 11157
*** empty log message ***
paulson [Fri, 16 Feb 2001 18:51:19 +0100] rev 11156
fixed the obvious errors Tobias found
paulson [Fri, 16 Feb 2001 18:50:09 +0100] rev 11155
Least_def now refers to LeastM
paulson [Fri, 16 Feb 2001 13:47:06 +0100] rev 11154
for the change to LEAST
paulson [Fri, 16 Feb 2001 13:37:21 +0100] rev 11153
Blast bug fix made old proof too slow
paulson [Fri, 16 Feb 2001 13:29:07 +0100] rev 11152
Blast bug fix: now always duplicates when applying a haz rule,
whether or not new variables are added.
Can now prove theorems such as these:
val prems = Goal "[|P==>Q; P==>~Q|] ==> ~P";
by (blast_tac (claset() addDs prems) 1);
val prems = Goal "[|Q==>P; ~Q==>P|] ==> P";
by (blast_tac (claset() addIs prems) 1);
paulson [Fri, 16 Feb 2001 13:27:56 +0100] rev 11151
Blast bug fix made old proof too slow
paulson [Fri, 16 Feb 2001 13:25:08 +0100] rev 11150
Streamlining for the bug fix in Blast.
MPair_parts now built in using AddSEs, throughout.
nipkow [Fri, 16 Feb 2001 08:27:17 +0100] rev 11149
*** empty log message ***
nipkow [Fri, 16 Feb 2001 08:10:28 +0100] rev 11148
*** empty log message ***
nipkow [Fri, 16 Feb 2001 06:46:20 +0100] rev 11147
*** empty log message ***
wenzelm [Fri, 16 Feb 2001 00:36:21 +0100] rev 11146
tuned;
wenzelm [Thu, 15 Feb 2001 17:18:54 +0100] rev 11145
eliminate get_def;
wenzelm [Thu, 15 Feb 2001 16:12:27 +0100] rev 11144
tuned;
oheimb [Thu, 15 Feb 2001 16:07:57 +0100] rev 11143
Ord.thy/.ML converted to Isar
oheimb [Thu, 15 Feb 2001 16:01:47 +0100] rev 11142
moved inv_image to Relation
nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML
added wf_linord_ex_has_least,LeastM_nat_lemma,LeastM_natI,LeastM_nat_le
oheimb [Thu, 15 Feb 2001 16:01:34 +0100] rev 11141
supressed some warnings on identical proofstate
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
from Nat.ML to Wellfounded_Recursion.ML
added wellorder axclass
oheimb [Thu, 15 Feb 2001 16:01:22 +0100] rev 11140
Ord.thy/.ML converted to Isar
added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy
moved Least_equality from Nat.ML to Ord.thy
added LeastM operator
oheimb [Thu, 15 Feb 2001 16:01:07 +0100] rev 11139
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
from Nat.ML to Wellfounded_Recursion.ML
moved Least_equality from Nat.ML to Ord.thy
moved wf_less from Nat.ML to NatDef.ML
added wellorder axclass
nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML
added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy
oheimb [Thu, 15 Feb 2001 16:00:44 +0100] rev 11138
simplified proof of Least_mono