convert-repo [Thu, 23 Jul 2009 14:03:20 +0000] rev 255
update tags
clasohm [Fri, 19 Jan 1996 12:50:08 +0100] rev 254
removed them again
clasohm [Fri, 19 Jan 1996 12:49:36 +0100] rev 253
accidentally deleted these files from the repository; now adding them and
"cvs rm"ing them again
clasohm [Fri, 19 Jan 1996 12:27:42 +0100] rev 252
Old_HOL removed from the distribution
clasohm [Tue, 24 Oct 1995 14:59:17 +0100] rev 251
added calls of init_html and make_chart
clasohm [Thu, 29 Jun 1995 12:29:58 +0200] rev 250
changed HOL to Old_HOL
clasohm [Wed, 21 Jun 1995 15:12:40 +0200] rev 249
removed \...\ inside strings
lcp [Fri, 14 Apr 1995 11:23:33 +0200] rev 248
Simplified some proofs and made them work for new hyp_subst_tac.
lcp [Thu, 06 Apr 1995 11:52:05 +0200] rev 247
Removed the "exit 1" calls, since now the
Makefile does them.
lcp [Thu, 06 Apr 1995 11:49:42 +0200] rev 246
Deleted extra space in clos_mk.
lcp [Thu, 06 Apr 1995 11:47:00 +0200] rev 245
Simplified some proofs and made them work for new hyp_subst_tac.
lcp [Thu, 06 Apr 1995 11:37:43 +0200] rev 244
Ran expandshort
lcp [Thu, 06 Apr 1995 11:35:33 +0200] rev 243
Removed the "exit 1" calls, since now the
Makefile does them.
lcp [Thu, 06 Apr 1995 11:32:47 +0200] rev 242
Deleted some useless things and made proofs of
refl_comp_subset and comp_equivI more like the versions in ZF/EquivClass.ML
lcp [Thu, 06 Apr 1995 11:27:54 +0200] rev 241
Removed the "exit 1" calls, since now the
Makefile does them.
lcp [Thu, 06 Apr 1995 11:24:11 +0200] rev 240
Set up for new hyp_subst_tac.
lcp [Thu, 06 Apr 1995 11:21:13 +0200] rev 239
Changed proof of lessE for new hyp_subst_tac
lcp [Thu, 06 Apr 1995 11:18:02 +0200] rev 238
Added Id: line
wenzelm [Fri, 31 Mar 1995 15:09:21 +0200] rev 237
replaced 'arities' by 'instance';
lcp [Thu, 30 Mar 1995 13:39:36 +0200] rev 236
Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)
clasohm [Tue, 28 Mar 1995 12:48:46 +0200] rev 235
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
apfst from Pure/library.ML
nipkow [Mon, 27 Mar 1995 18:30:04 +0200] rev 234
Added recursion equations for foldl to list_ss.
nipkow [Fri, 17 Mar 1995 15:48:55 +0100] rev 233
Added a few thms to nat_ss and list_ss
lcp [Wed, 15 Mar 1995 10:44:26 +0100] rev 232
Now calls exit_use instead of use, for prompt failure if errors are detected.
nipkow [Tue, 14 Mar 1995 09:43:12 +0100] rev 231
Removed some type constraints
nipkow [Tue, 14 Mar 1995 09:42:49 +0100] rev 230
added "exit 1"
nipkow [Mon, 13 Mar 1995 09:41:20 +0100] rev 229
Removed unecessary type constraint because instantiations do not freeze type
vars any more.
nipkow [Wed, 08 Mar 1995 17:22:28 +0100] rev 228
Added dependencies on ../Provers/hypsubst.ML and removed those on
../Provers/ind.ML
nipkow [Wed, 08 Mar 1995 13:06:44 +0100] rev 227
Enforced partial evaluation of mk_case_split_tac
lcp [Wed, 01 Mar 1995 17:44:05 +0100] rev 226
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
Moved less_leq_less from IOA/example/Lemmas to Nat.ML as less_le_trans.
lcp [Wed, 01 Mar 1995 17:37:09 +0100] rev 225
Proofs of inv1 and inv4 now use less_le_trans instead of
less_leq_less.
lcp [Wed, 01 Mar 1995 17:32:10 +0100] rev 224
Renamed plus_leD1 to add_leD1.
lcp [Wed, 01 Mar 1995 13:26:50 +0100] rev 223
Proved inj_onto_iff
lcp [Tue, 28 Feb 1995 10:52:55 +0100] rev 222
No longer calls maketest; instead, the Makefile writes the file
"test". And had to delete an extra ).
lcp [Tue, 28 Feb 1995 10:48:46 +0100] rev 221
Re-organised to perform the tests independently. Now test
is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set
wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to
refer to the right command for running the object-logic. Uses "suffix
substitution" to shorten macro definitions.
lcp [Tue, 28 Feb 1995 02:02:34 +0100] rev 220
Installation of Integ (ported from ZF by Mattolini)
lcp [Tue, 28 Feb 1995 02:00:28 +0100] rev 219
Proved less_eq_Suc_add and add_left_cancel (cf left_plus_cancel on
IOA/example/Lemmas). Proved add_left_cancel_le and add_left_cancel_less.
Proved trans_le_add1,2 and trans_less_add1,2 (cxf leq_add_leq in
IOA/example/Lemmas). Renamed plus_leD1 to add_leD1. Moved diff_le_self and
monotonicity theorems from ZF/Arith.ML
lcp [Mon, 27 Feb 1995 17:20:33 +0100] rev 218
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
Moved less_leq_less from IOA/example/Lemmas to Nat.ML as less_le_trans.
lcp [Mon, 27 Feb 1995 16:46:38 +0100] rev 217
Installation of Integ (ported from ZF by Mattolini)
lcp [Mon, 27 Feb 1995 16:36:17 +0100] rev 216
Installation of Integ (ported from ZF by Mattolini)
nipkow [Sun, 19 Feb 1995 15:04:39 +0100] rev 215
Reorganized/optimized datatype definitions.
nipkow [Thu, 16 Feb 1995 08:56:44 +0100] rev 214
pair_ss -> prod_ss.
nipkow [Thu, 16 Feb 1995 08:56:21 +0100] rev 213
Removed pair_ss because identical to prod_ss.
nipkow [Mon, 13 Feb 1995 15:12:08 +0100] rev 212
Added "flat"
nipkow [Wed, 08 Feb 1995 14:06:37 +0100] rev 211
Norbert's update allowing nested calls in primrec.
nipkow [Wed, 08 Feb 1995 11:34:11 +0100] rev 210
More rewrite rules.
nipkow [Fri, 03 Feb 1995 16:21:45 +0100] rev 209
Add dependence on ex/String.thy/ML
nipkow [Fri, 03 Feb 1995 16:19:45 +0100] rev 208
Added Markus Wenzel's string representation.
nipkow [Wed, 01 Feb 1995 17:18:00 +0100] rev 207
Simplified proof.
nipkow [Wed, 01 Feb 1995 17:17:35 +0100] rev 206
The thm if(P,Q,R) now yields the two conditional rewrite rules P ==> Q and
P ==> R.
nipkow [Mon, 30 Jan 1995 16:32:32 +0100] rev 205
Added Un_empty (also to set_ss)
nipkow [Sun, 29 Jan 1995 14:02:17 +0100] rev 204
Added some simplifications for ? x.
nipkow [Thu, 26 Jan 1995 10:41:21 +0100] rev 203
Added "nth" and some lemmas.
clasohm [Wed, 14 Dec 1994 11:17:18 +0100] rev 202
added bind_thm for theorems made by "standard ..."
wenzelm [Wed, 14 Dec 1994 10:32:07 +0100] rev 201
improved primrec: now calls store_thm;
clasohm [Fri, 09 Dec 1994 13:39:05 +0100] rev 200
removed HOL_Lemmas structure and added qed_goal
clasohm [Thu, 08 Dec 1994 12:50:38 +0100] rev 199
replaced store_thm by bind_thm
nipkow [Wed, 07 Dec 1994 14:12:27 +0100] rev 198
Added (? x. x=t & P) = P to the simpset.
nipkow [Wed, 07 Dec 1994 14:11:22 +0100] rev 197
Removed a local lemma which is now part of HOL_ss.
nipkow [Fri, 02 Dec 1994 16:13:34 +0100] rev 196
Moved the old List to ex and replaced it by one defined via
datatype and primrec. List does not depend on Sexp any more.
Had to modify the datatype-grammar to allow "[]" ("[]"). Does not allow
strings but only ids as type constructors. This is consistent with the
documentation and merely undoes an extension of Markus's.
nipkow [Fri, 02 Dec 1994 16:09:49 +0100] rev 195
Moved HOL/List to HOL/ex/SList (strict list).
Modified sons on (S)List accordingly.
nipkow [Fri, 02 Dec 1994 11:43:20 +0100] rev 194
small updates because datatype list is now used. In particular Nil -> []
nipkow [Fri, 02 Dec 1994 10:26:59 +0100] rev 193
list_ind_tac -> list.induct_tac
nipkow [Thu, 01 Dec 1994 17:35:03 +0100] rev 192
Added dependency on thy_syntax.ML
nipkow [Mon, 28 Nov 1994 16:45:29 +0100] rev 191
Fixed small bug in print-translation for set comprehension.
wenzelm [Mon, 28 Nov 1994 14:42:42 +0100] rev 190
adapted to 'subtype' section;
nipkow [Fri, 25 Nov 1994 20:07:22 +0100] rev 189
added IMP/Properties
nipkow [Fri, 25 Nov 1994 20:06:15 +0100] rev 188
Proved determinism.
wenzelm [Fri, 25 Nov 1994 16:24:18 +0100] rev 187
minor changes according to new hologic;
wenzelm [Fri, 25 Nov 1994 14:39:13 +0100] rev 186
replaced ["term"] by termS;
wenzelm [Fri, 25 Nov 1994 14:21:14 +0100] rev 185
adapted to 'subtype' section;
cleaned up;
nipkow [Fri, 25 Nov 1994 13:35:32 +0100] rev 184
added id_in_pair_conv
nipkow [Fri, 25 Nov 1994 13:34:33 +0100] rev 183
Removed obsolete induction package
nipkow [Fri, 25 Nov 1994 13:33:27 +0100] rev 182
removed Sum-rules
lcp [Fri, 25 Nov 1994 11:10:26 +0100] rev 181
checks that the recursive sets are Consts before taking
them apart! Bug was introduced during the translation to theory sections.
nipkow [Fri, 25 Nov 1994 09:59:51 +0100] rev 180
renamed term_induct/2 -> Term_induct/2
clasohm [Fri, 25 Nov 1994 09:12:16 +0100] rev 179
replaced prove_goal by qed_goal
nipkow [Thu, 24 Nov 1994 20:31:09 +0100] rev 178
rules -> defs
nipkow [Thu, 24 Nov 1994 20:11:40 +0100] rev 177
The collection of theories required for inductive definitions.
nipkow [Thu, 24 Nov 1994 20:00:52 +0100] rev 176
Trancl.{thy,ML} was missing
wenzelm [Wed, 23 Nov 1994 15:09:44 +0100] rev 175
moved parser stuff to thy_syntax.ML;
wenzelm [Wed, 23 Nov 1994 10:41:42 +0100] rev 174
add_subtype now adds constant definition for the representing set;
wenzelm [Wed, 23 Nov 1994 10:37:27 +0100] rev 173
moved remaining thy syntax stuff to thy_syntax.ML;
wenzelm [Wed, 23 Nov 1994 10:36:03 +0100] rev 172
added 'datatype' and 'primrec';
subtype: added axiom <tyname>_def;
clasohm [Mon, 21 Nov 1994 17:50:34 +0100] rev 171
replaced 'val ... = result()' by 'qed "..."'
lcp [Fri, 11 Nov 1994 10:35:03 +0100] rev 170
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
ensures that if one dies, all die. BUT NOT Pure/Makefile, where
PolyML.use"POLY" makes the identifier "use" visible.
nipkow [Thu, 10 Nov 1994 09:46:19 +0100] rev 169
Initial revision
nipkow [Wed, 09 Nov 1994 19:51:09 +0100] rev 168
Added headers and made various small mods.
nipkow [Wed, 09 Nov 1994 19:50:36 +0100] rev 167
Added header.
lcp [Tue, 08 Nov 1994 11:21:33 +0100] rev 166
HOL/ROOT/HOL_dup_cs: removed as obsolete
HOL/ROOT: now passes "classical" to Classical_Fun
HOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac
clasohm [Sun, 06 Nov 1994 21:04:50 +0100] rev 165
changed loadpath
clasohm [Sun, 06 Nov 1994 21:04:39 +0100] rev 164
changed command for making 'test'
wenzelm [Fri, 04 Nov 1994 14:19:30 +0100] rev 163
rearranged theory section stuff;
added hologic.ML, subtype.ML;
wenzelm [Fri, 04 Nov 1994 14:17:20 +0100] rev 162
moved section parser to thy_syntax.ML;
wenzelm [Fri, 04 Nov 1994 14:16:39 +0100] rev 161
lnternal interface for HOL subtype definitions;
wenzelm [Fri, 04 Nov 1994 14:15:29 +0100] rev 160
additional theory file sections for HOL;
wenzelm [Fri, 04 Nov 1994 14:14:22 +0100] rev 159
abstract syntax operations for HOL;
nipkow [Thu, 03 Nov 1994 11:36:54 +0100] rev 158
Replaced fast_tac by simp_tac in a number of places.
Shorter and almost 20% faster.
clasohm [Wed, 02 Nov 1994 15:26:13 +0100] rev 157
added IOA files
clasohm [Wed, 02 Nov 1994 11:50:09 +0100] rev 156
added IOA to isabelle/HOL
lcp [Tue, 01 Nov 1994 11:00:45 +0100] rev 155
HOL/HOL/swap: deleted
HOL/HOL/classical: simpler proof
lcp [Mon, 31 Oct 1994 17:17:48 +0100] rev 154
HOL/ex/cla: proofs now use deepen_tac instead of best_tac HOL_dup_cs
lcp [Thu, 13 Oct 1994 09:39:15 +0100] rev 153
HOL/HOL.ML/selectI2: new rule for descriptions
lcp [Wed, 12 Oct 1994 12:06:56 +0100] rev 152
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
solve the goal fully before proceeding
{HOL,ZF}/indrule/mutual_ind_tac: ensures that calls to "prem" cannot loop;
calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully
lcp [Wed, 12 Oct 1994 12:00:45 +0100] rev 151
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
solve the goal fully before proceeding
{HOL,ZF}/indrule/mutual_ind_tac: ensures that calls to "prem" cannot loop;
calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully
nipkow [Thu, 06 Oct 1994 09:36:40 +0100] rev 150
replaced some "rules" by "defs"
clasohm [Tue, 04 Oct 1994 13:00:20 +0100] rev 149
changed precedences to eliminate some ambiguities
nipkow [Wed, 28 Sep 1994 12:39:32 +0100] rev 148
moved LList* to ex
nipkow [Tue, 27 Sep 1994 13:23:04 +0100] rev 147
Small simplification in add_datatype.
small simplification in add_primrec
nipkow [Mon, 26 Sep 1994 18:04:43 +0100] rev 146
replaced local instantaite_types by inferT_axm
wenzelm [Wed, 21 Sep 1994 15:40:41 +0200] rev 145
minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections;
nipkow [Fri, 16 Sep 1994 15:48:20 +0200] rev 144
Definition of C was not truly prim rec because C was called inside Gamma
instead of outside.
nipkow [Thu, 15 Sep 1994 18:42:12 +0200] rev 143
improved error reporting for primrec
wenzelm [Wed, 14 Sep 1994 16:05:28 +0200] rev 142
replaced lookup_const by Sign.const_type;
nipkow [Sun, 11 Sep 1994 10:31:17 +0200] rev 141
Allowed string as function name in primrec header
lcp [Thu, 08 Sep 1994 11:01:45 +0200] rev 140
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
separate call to hyp_subst_tac. This avoids substituting in x=f(x)
{HOL,ZF}/indrule/ind_tac: now tries resolve_tac [refl]. This handles
trivial equalities such as x=a.
{HOL,ZF}/intr_elim/intro_tacsf_tac: now calls assume_tac last, to try refl
before any equality assumptions
lcp [Wed, 07 Sep 1994 13:17:34 +0200] rev 139
HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster
nipkow [Tue, 06 Sep 1994 16:46:27 +0200] rev 138
changed names
nipkow [Tue, 06 Sep 1994 16:15:59 +0200] rev 137
Converted rules to primrecs
lcp [Tue, 06 Sep 1994 13:24:29 +0200] rev 136
corrected comment re treatment of types such as (bool*bool)*bool
lcp [Tue, 06 Sep 1994 10:56:54 +0200] rev 135
HOL/ex/PropLog.thy: tidied
lcp [Tue, 06 Sep 1994 10:54:46 +0200] rev 134
HOL/ind_syntax/factors: now returns only factors in the product type that
associate to the right. Previously the proof of the induction rule
crashed on types such as (bool*bool)*bool.
nipkow [Wed, 31 Aug 1994 17:50:59 +0200] rev 133
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
Improved layout for set comprehension in Set.thy.
nipkow [Wed, 31 Aug 1994 16:25:19 +0200] rev 132
Renamed a few types and vars
nipkow [Wed, 31 Aug 1994 15:15:54 +0200] rev 131
Equivalence of op. and den. sem. for simple while language.
nipkow [Tue, 30 Aug 1994 10:05:46 +0200] rev 130
Updated PL to PropLog using Larrys ind. defs.
nipkow [Tue, 30 Aug 1994 10:04:49 +0200] rev 129
New version of datatype.ML with primrec (Norbert).
Updated treatment of bounded quantifiers in the simplifier.
lcp [Thu, 25 Aug 1994 11:01:45 +0200] rev 128
INSTALLATION OF INDUCTIVE DEFINITIONS
HOL/Sexp, List, LList: updated for inductive defs; streamlined proofs
HOL/List, Subst/UTerm, ex/Simult, ex/Term: updated refs to Sexp intr rules
HOL/Univ/diag_eqI: new
HOL/intr_elim: now checks that the inductive name does not clash with
existing theory names
HOL/Sum: now type + is an infixr, to agree with type *
HOL/Set: added Pow and the derived rules PowI, PowD, Pow_bottom, Pow_top
HOL/Fun/set_cs: now includes Pow rules
HOL/mono/Pow_mono: new
HOL/Makefile: now has Inductive.thy,.ML and ex/Acc.thy,.ML
HOL/Sexp,List,LList,ex/Term: converted as follows
node *set -> item
Sexp -> sexp
LList_corec -> <self>
LList_ -> llist_
LList\> -> llist
List_case -> <self>
List_rec -> <self>
List_ -> list_
List\> -> list
Term_rec -> <self>
Term_ -> term_
Term\> -> term
lcp [Thu, 25 Aug 1994 10:47:33 +0200] rev 127
INSTALLATION OF INDUCTIVE DEFINITIONS
HOL/ex/MT.thy: now mentions dependence upon Sum.thy
HOL/ex/Acc: new example, borrowed & adapted from ZF
HOL/ex/Simult, ex/Term: updated refs to Sexp intr rules
HOL/Sexp,List,LList,ex/Term: converted as follows
node *set -> item
Sexp -> sexp
LList_corec -> <self>
LList_ -> llist_
LList\> -> llist
List_case -> <self>
List_rec -> <self>
List_ -> list_
List\> -> list
Term_rec -> <self>
Term_ -> term_
Term\> -> term
lcp [Wed, 24 Aug 1994 18:49:29 +0200] rev 126
Subst/UTerm: updated for inductive defs; streamlined proofs
lcp [Mon, 22 Aug 1994 12:00:02 +0200] rev 125
HOL/ex/MT.thy: now mentions dependence upon Sum.thy
lcp [Mon, 22 Aug 1994 11:54:23 +0200] rev 124
new header & minor changes
lcp [Mon, 22 Aug 1994 11:02:35 +0200] rev 123
changed defn to def
lcp [Mon, 22 Aug 1994 10:56:45 +0200] rev 122
HOL/Sum.thy: generalized the type of Part
wenzelm [Fri, 19 Aug 1994 16:18:44 +0200] rev 121
replaced add_defns_i by add_defs_i;
changed instant_types: now uses Sign.infer_types;
lcp [Fri, 19 Aug 1994 11:27:19 +0200] rev 120
HOL/Trancl.thy: depends upon Prod
lcp [Fri, 19 Aug 1994 11:25:16 +0200] rev 119
HOL/Makefile, ROOT: updated for new .thy files
lcp [Fri, 19 Aug 1994 11:19:14 +0200] rev 118
HOL/Ord.thy,.ML: files now have header comments
lcp [Fri, 19 Aug 1994 11:15:01 +0200] rev 117
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
overloaded with an incompatible type
lcp [Fri, 19 Aug 1994 11:10:56 +0200] rev 116
HOL/subset.thy, equalities.thy, mono.thy: new
HOL/Lfp.thy: now depends upon mono
HOL/Gfp.thy: depends upon Lfp, not just mono
lcp [Fri, 19 Aug 1994 11:02:45 +0200] rev 115
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp [Thu, 18 Aug 1994 12:48:03 +0200] rev 114
HOL/ex/Term, Simult: updated for new Split
lcp [Thu, 18 Aug 1994 12:42:19 +0200] rev 113
HOL/List: rotated arguments of List_case, list_case
lcp [Thu, 18 Aug 1994 12:38:12 +0200] rev 112
HOL/Prod: swapped args of split and simplified
HOL/Prod/mem_splitI, mem_splitE, prod_cs: new
lcp [Thu, 18 Aug 1994 12:23:52 +0200] rev 111
HOL/Univ: swapped args of split and simplified
HOL/Univ: simplified many proofs involving dprod, dsum.
HOL/Univ: updated to new nat_case
HOL/Univ/univ_cs: added to it and used it more
lcp [Thu, 18 Aug 1994 12:13:26 +0200] rev 110
HOL/Sexp: rotated arguments of Sexp_case
lcp [Thu, 18 Aug 1994 12:07:51 +0200] rev 109
HOL/Nat: rotated arguments of nat_case; added translation for case macro
HOL/Nat/nat_ss0: new, for first definition of nat_ss
lcp [Thu, 18 Aug 1994 11:54:20 +0200] rev 108
HOL/Trancl: comp_cs is based upon prod_cs; tidied proofs
lcp [Thu, 18 Aug 1994 11:43:40 +0200] rev 107
HOL/Sum: rotated arguments of sum_case; added translation for case macro
HOL/Sum: now has Part primitives, moved from ex/Simult, with extra
laws from ZF/Sum
lcp [Thu, 18 Aug 1994 11:40:54 +0200] rev 106
HOL/Subst/AList: swapped args of split and simplified
lcp [Thu, 18 Aug 1994 11:30:27 +0200] rev 105
HOL/LList: swapped args of split and simplified
HOL/List: rotated arguments of List_case, list_case
HOL/LList: rotated arguments of llist_case (shares List_case) and tidied
many proofs
nipkow [Tue, 16 Aug 1994 09:57:51 +0200] rev 104
allow long_id for reference to type in primrec.
Doesn't work yet, though, because of problems with the autoloader.
nipkow [Mon, 15 Aug 1994 15:20:34 +0200] rev 103
Cleaned up code.
nipkow [Sat, 13 Aug 1994 16:34:30 +0200] rev 102
Used the new primitive recursive functions format for thy-files
nipkow [Sat, 13 Aug 1994 16:33:53 +0200] rev 101
Added primitive recursive functions (Norbert Voelker's code) to the datatype
package.
nipkow [Wed, 03 Aug 1994 11:00:40 +0200] rev 100
renamed meta_obj_reflection meta_eq_to_obj_eq.
nipkow [Tue, 02 Aug 1994 16:43:39 +0200] rev 99
exposed meta_obj_reflection
lcp [Wed, 27 Jul 1994 19:08:40 +0200] rev 98
added a new example due to Robin Arthan
lcp [Thu, 21 Jul 1994 10:52:00 +0200] rev 97
HOL/Makefile: now test depends upon SUBST_FILES
HOL/Makefile/SUBST_FILES: changed some filenames to upper case
HOL/Makefile: now executes ex/ROOT.ML after Subst/ROOT.ML
nipkow [Fri, 15 Jul 1994 14:04:28 +0200] rev 96
Lots of simplifications
nipkow [Fri, 15 Jul 1994 13:53:18 +0200] rev 95
added val eq_sym_conv = prover "(x=y) = (y=x)";
lcp [Tue, 12 Jul 1994 16:34:45 +0200] rev 94
fixed indentation
nipkow [Fri, 08 Jul 1994 17:39:02 +0200] rev 93
Integrated PL0.thy into PL.thy
nipkow [Fri, 08 Jul 1994 17:22:58 +0200] rev 92
Hidden dtK and Impossible with a "local" clause
clasohm [Fri, 08 Jul 1994 12:01:55 +0200] rev 91
added mixfix annotations to constructor declarations
clasohm [Wed, 29 Jun 1994 12:04:04 +0200] rev 90
added parentheses made necessary by change of constrain's precedence
lcp [Fri, 24 Jun 1994 15:11:39 +0200] rev 89
HOL/Nat/less_asym: renamed from less_anti_sym
lcp [Fri, 24 Jun 1994 15:10:13 +0200] rev 88
HOL/WF/wf_asym: renamed from wf_anti_sym
clasohm [Mon, 20 Jun 1994 14:52:40 +0200] rev 87
added prefix to name of induct axiom
nipkow [Mon, 20 Jun 1994 12:05:03 +0200] rev 86
Datatype -> Datatype.ML
lcp [Fri, 17 Jun 1994 18:34:12 +0200] rev 85
HOL/Arith/add_left_commute: tidied
HOL/Arith/add_mult_distrib: DELETED DUPLICATE COPY
lcp [Fri, 17 Jun 1994 18:32:25 +0200] rev 84
HOL/HOL.ML/notE: tidied the proof
lcp [Fri, 17 Jun 1994 18:30:18 +0200] rev 83
HOL/List/map_append,map_compose: new
lcp [Fri, 17 Jun 1994 18:28:36 +0200] rev 82
HOL/ex/NatSum: added another example
clasohm [Fri, 17 Jun 1994 14:16:50 +0200] rev 81
adopted to new datatype definition method
clasohm [Fri, 17 Jun 1994 14:15:38 +0200] rev 80
datatypes must now be defined using a thy file section
nipkow [Wed, 15 Jun 1994 19:28:35 +0200] rev 79
Added set comprehension as a syntactic abbreviation:
{e | x1..xn. P} means {u. ? x1 .. xn. u=e & P}
lcp [Wed, 01 Jun 1994 13:24:54 +0200] rev 78
added test for $ISABELLEBIN=source directory, to
avoid isabelle/Pure being mistaken for bin/Pure
lcp [Wed, 25 May 1994 13:03:19 +0200] rev 77
HOL/Arith: definition of diff now uses pred, not nat_rec
lcp [Wed, 25 May 1994 12:43:50 +0200] rev 76
HOL/equalities: added some identities from ZF/equalities
HOL/equalities/constant_UN: renamed UN1_constant
HOL/equalities/Union_Un_distrib: deleted duplicate!
HOL/equalities/Union_Int_subset: new
lcp [Wed, 25 May 1994 12:25:40 +0200] rev 75
HOL/HOL.ML/notE: tidied
wenzelm [Thu, 19 May 1994 17:07:19 +0200] rev 74
thy reader now initialised by init_thy_reader();
lcp [Fri, 13 May 1994 11:14:20 +0200] rev 73
HOL/Prod/pair_eq: renamed to Pair_fst_snd_eq
lcp [Tue, 03 May 1994 15:48:19 +0200] rev 72
removal of obsolete type-declaration syntax
lcp [Tue, 03 May 1994 11:30:09 +0200] rev 71
removal of obsolete type-declaration syntax
clasohm [Sun, 24 Apr 1994 11:27:38 +0200] rev 70
renamed theory files
clasohm [Fri, 22 Apr 1994 21:23:14 +0200] rev 69
renamed theory files
lcp [Thu, 21 Apr 1994 11:28:32 +0200] rev 68
tidied definitions and proofs
lcp [Thu, 21 Apr 1994 11:13:22 +0200] rev 67
HOL/arith.ML/plus_leD1: tidied
nipkow [Tue, 19 Apr 1994 10:50:00 +0200] rev 66
changed defns in hol.thy from = to ==
lcp [Wed, 06 Apr 1994 16:31:06 +0200] rev 65
Now simplifies before the induction
nipkow [Wed, 30 Mar 1994 10:00:23 +0200] rev 64
@ now associates to the right, just like #, in order to avoid loss of
parentheses due to pretty printer.
nipkow [Sun, 27 Mar 1994 16:43:06 +0200] rev 63
Added some sums.
nipkow [Sun, 27 Mar 1994 12:36:39 +0200] rev 62
integrated permutative rewriting
nipkow [Tue, 22 Mar 1994 19:55:29 +0100] rev 61
used new field "simps" of Datatype
nipkow [Tue, 22 Mar 1994 19:54:55 +0100] rev 60
new field "simps" added
nipkow [Tue, 22 Mar 1994 18:07:45 +0100] rev 59
added dependency on datatype.ML
nipkow [Tue, 22 Mar 1994 08:32:22 +0100] rev 58
Updated simpsets and a few proofs.
nipkow [Tue, 22 Mar 1994 08:31:58 +0100] rev 57
Updated simpsets and a few proofs.
Reomved junk file test.ML.
nipkow [Tue, 22 Mar 1994 08:28:31 +0100] rev 56
Used Datatype functor to define propositional logic terms.
nipkow [Tue, 22 Mar 1994 08:26:25 +0100] rev 55
simplified some proofs using ordered rewriting.
nipkow [Tue, 22 Mar 1994 08:25:30 +0100] rev 54
used ordered rewriting to simplify some proofs
nipkow [Fri, 18 Mar 1994 20:33:32 +0100] rev 53
ML-like datatype decalaration facility. Axiomatic.
nipkow [Fri, 18 Mar 1994 20:32:18 +0100] rev 52
added use_thy"Datatype"
lcp [Thu, 17 Mar 1994 17:02:49 +0100] rev 51
new type declaration syntax instead of numbers
lcp [Thu, 17 Mar 1994 14:08:08 +0100] rev 50
HOL/equalities/Int_Union_image, Un_Inter_image: renamed Int_Union, Un_Inter
as they do not refer to images.
clasohm [Thu, 17 Mar 1994 11:27:29 +0100] rev 49
adapted type definition to new syntax
clasohm [Wed, 02 Mar 1994 12:26:55 +0100] rev 48
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
nipkow [Thu, 24 Feb 1994 14:45:57 +0100] rev 47
typo in comment
nipkow [Wed, 23 Feb 1994 10:05:35 +0100] rev 46
some more sorting algorithms
nipkow [Wed, 16 Feb 1994 15:13:53 +0100] rev 45
added more lemmas (also to nat_ss)
nipkow [Tue, 15 Feb 1994 10:05:17 +0100] rev 44
deleted duplicate rewrite rules
nipkow [Tue, 15 Feb 1994 07:55:22 +0100] rev 43
added etac FalseE to the simplifier's solver.
nipkow [Sat, 12 Feb 1994 14:46:21 +0100] rev 42
added translations for "case xs of"
nipkow [Fri, 11 Feb 1994 11:09:50 +0100] rev 41
added ::bool in the defn of True.
nipkow [Thu, 03 Feb 1994 09:55:47 +0100] rev 40
Introduction of various new lemmas and of case_tac.
nipkow [Thu, 27 Jan 1994 17:01:10 +0100] rev 39
id -> idt in type of @filter and @Alls
nipkow [Wed, 26 Jan 1994 17:53:27 +0100] rev 38
sum: renamed case to sum_case
hol: added general case-of syntax
nipkow [Mon, 24 Jan 1994 16:03:03 +0100] rev 37
changed header
nipkow [Mon, 24 Jan 1994 16:00:37 +0100] rev 36
Verification of quicksort
nipkow [Mon, 24 Jan 1994 15:59:44 +0100] rev 35
added qsort
nipkow [Mon, 24 Jan 1994 15:59:02 +0100] rev 34
added conj_assoc to HOL_ss
added filter, mem, and some syntax to lists
lcp [Fri, 14 Jan 1994 12:35:27 +0100] rev 33
commented imageE
nipkow [Fri, 07 Jan 1994 14:23:13 +0100] rev 32
added let_weak_cong
nipkow [Fri, 07 Jan 1994 14:22:37 +0100] rev 31
added pair_eq
nipkow [Wed, 05 Jan 1994 19:39:05 +0100] rev 30
modified solver of HOL_ss to take the new simplifier into account: the thm to
be solved may have assumption.
nipkow [Wed, 05 Jan 1994 19:37:07 +0100] rev 29
added new rewrite rules to arith_ss
nipkow [Tue, 04 Jan 1994 18:33:20 +0100] rev 28
shortened use_thy section taking advantage of dependencies
nipkow [Thu, 30 Dec 1993 10:19:44 +0100] rev 27
added x ~: {} and x : insert(y,A) = ...
nipkow [Wed, 22 Dec 1993 12:43:37 +0100] rev 26
added Pair_eq to pair_ss in prod.ML
removed it locally in llist.ML because preconditions of the form <a,b> =
<?x,?y>, which used to be solved by reflexivity, now rewrote to a = ?x & b =
?y, which is not solved by reflexivity.
nipkow [Tue, 14 Dec 1993 18:05:22 +0100] rev 25
added syntax for nested lets.
lcp [Mon, 13 Dec 1993 18:43:03 +0100] rev 24
added mention of Subst
lcp [Fri, 03 Dec 1993 12:41:54 +0100] rev 23
added new example
lcp [Wed, 01 Dec 1993 13:05:25 +0100] rev 22
HOL/llist/LList_corec_subset1: does not need induction
nipkow [Tue, 30 Nov 1993 17:44:04 +0100] rev 21
added pred: nat=>nat
nipkow [Mon, 29 Nov 1993 18:35:02 +0100] rev 20
changed simpsets
nipkow [Thu, 25 Nov 1993 10:04:02 +0100] rev 19
added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
lcp [Fri, 19 Nov 1993 11:36:23 +0100] rev 18
Trivial spacing corrections
clasohm [Tue, 16 Nov 1993 14:14:22 +0100] rev 17
changed use_thy's parameter to exact theory name
lcp [Tue, 09 Nov 1993 16:31:03 +0100] rev 16
Target "test" now depends on examples files
clasohm [Tue, 09 Nov 1993 13:30:13 +0100] rev 15
renamed meson-test.ML to mesontest.ML,
used exact theory names for use_thy
lcp [Tue, 09 Nov 1993 11:08:13 +0100] rev 14
co-induction example courtesy Jacob Frost
nipkow [Wed, 03 Nov 1993 19:02:17 +0100] rev 13
added append "@"
Proved @ associativ
wenzelm [Mon, 25 Oct 1993 14:36:27 +0100] rev 12
added white-space;
made ~: a fake infix;
wenzelm [Mon, 25 Oct 1993 14:35:17 +0100] rev 11
made ~= a fake infix;
clasohm [Fri, 22 Oct 1993 13:36:28 +0100] rev 10
changes for new Readthy
clasohm [Sun, 17 Oct 1993 17:33:40 +0100] rev 9
renamed: hol-rec.* to rec.*, lex-prod.* to lexprod.*, prop-log.* to pl.*
clasohm [Sun, 17 Oct 1993 17:23:51 +0100] rev 8
renamed utermlemmas.* to utlemmas.*
wenzelm [Fri, 08 Oct 1993 13:46:13 +0100] rev 7
removed THE;
lcp [Thu, 07 Oct 1993 10:29:23 +0100] rev 6
used ~= for "not equals" and ~: for "not in"
lcp [Thu, 07 Oct 1993 10:20:30 +0100] rev 5
added ~= for "not equals" and added ~: for "not in"
wenzelm [Mon, 04 Oct 1993 15:43:54 +0100] rev 4
HOL/hol.thy
renamed mk_alt_ast_tr' to alt_ast_tr';
added alternative quantifier THE;
replaced Ast by Syntax;
HOL/set.thy
replaced HOL.mk_alt_ast_tr' by HOL.alt_ast_tr';
lcp [Tue, 28 Sep 1993 14:27:31 +0100] rev 3
This repeats a previous commit, which failed to update simpdata.ML because
a lock file was present.
lcp [Wed, 22 Sep 1993 15:43:05 +0200] rev 2
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
split_weak_cong, nat_case_weak_cong, nat_rec_weak_cong. Used in llist.ML
to make simplifications faster.
HOL/gfp: re-ordered premises to put mono(f) early (first or right after
A==gfp(f) in the def_ rules). Renamed some variables in rules, A to X and
h to A. Renamed coinduct to weak_coinduct, coinduct2 to coinduct.
Strengthened coinduct as suggested by j. Frost, to have the premise X <= f(X
Un gfp(f)).
HOL/llist: used stronger coinduct rule to strengthen LList_coinduct,
LList_equalityI, llist_equalityI, llist_fun_equalityI and to delete the "2"
form of those rules. Proved List_Fun_LList_I, LListD_Fun_diag_I and
llistD_Fun_range_I to help use the new coinduction rules; most proofs
involving them required small changes. Proved prod_fun_range_eq_diag as
lemma for llist_equalityI.
nipkow [Thu, 16 Sep 1993 14:29:14 +0200] rev 1
defined addcongs locally in simpdata.ML
clasohm [Thu, 16 Sep 1993 12:21:07 +0200] rev 0
Initial revision