huffman [Fri, 20 Jun 2008 22:51:50 +0200] rev 27309
clean up and rename some profinite lemmas
isatest [Fri, 20 Jun 2008 22:41:41 +0200] rev 27308
move at-sml-dev-e to macbroy23
huffman [Fri, 20 Jun 2008 22:28:10 +0200] rev 27307
replace SetPcpo.thy with Cset.thy
wenzelm [Fri, 20 Jun 2008 22:02:33 +0200] rev 27306
updated for 2008;
proper name of TUM;
haftmann [Fri, 20 Jun 2008 21:01:17 +0200] rev 27305
(removed non-present change)
haftmann [Fri, 20 Jun 2008 21:00:28 +0200] rev 27304
explicit thm context for error messages
haftmann [Fri, 20 Jun 2008 21:00:27 +0200] rev 27303
using tages to find theory names
haftmann [Fri, 20 Jun 2008 21:00:26 +0200] rev 27302
type constructors now with markup
haftmann [Fri, 20 Jun 2008 21:00:25 +0200] rev 27301
fixed bind error for malformed primrec specifications
haftmann [Fri, 20 Jun 2008 21:00:22 +0200] rev 27300
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann [Fri, 20 Jun 2008 21:00:21 +0200] rev 27299
streamlined definitions
haftmann [Fri, 20 Jun 2008 21:00:16 +0200] rev 27298
moved Float.thy to Library
huffman [Fri, 20 Jun 2008 20:03:13 +0200] rev 27297
removed SetPcpo.thy and cpo instance for type bool;
added Cset.thy with pcpo type 'a cset isomorphic to 'a set;
updated ideal completion theory to use cset
huffman [Fri, 20 Jun 2008 19:59:00 +0200] rev 27296
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
huffman [Fri, 20 Jun 2008 19:57:45 +0200] rev 27295
add lemma Abs_image
huffman [Fri, 20 Jun 2008 18:03:01 +0200] rev 27294
added some lemmas; reorganized into sections; tuned proofs
huffman [Fri, 20 Jun 2008 18:00:55 +0200] rev 27293
added some lemmas; tuned proofs
huffman [Fri, 20 Jun 2008 17:58:16 +0200] rev 27292
tuned
huffman [Fri, 20 Jun 2008 17:56:00 +0200] rev 27291
replace less_lift with flat_less_iff
huffman [Fri, 20 Jun 2008 17:43:16 +0200] rev 27290
tweak lemmas adm_all and adm_ball
huffman [Thu, 19 Jun 2008 22:50:58 +0200] rev 27289
move lemmas into locales;
restructure some proofs
huffman [Thu, 19 Jun 2008 22:43:59 +0200] rev 27288
add lemmas take_chain_less and take_chain_le
wenzelm [Thu, 19 Jun 2008 22:27:10 +0200] rev 27287
disposed Sign.read_typ etc;
wenzelm [Thu, 19 Jun 2008 22:05:05 +0200] rev 27286
renamed is_abbrev_mode to abbrev_mode;
added private get_sort (from sign.ML);
wenzelm [Thu, 19 Jun 2008 22:05:04 +0200] rev 27285
ProofContext.abbrev_mode;
wenzelm [Thu, 19 Jun 2008 22:05:01 +0200] rev 27284
moved get_sort to Isar/proof_context.ML;
removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;
wenzelm [Thu, 19 Jun 2008 21:14:30 +0200] rev 27283
tuned signature;
removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);
wenzelm [Thu, 19 Jun 2008 20:48:06 +0200] rev 27282
private add_used (from drule.ML);
Variable.declare_names;
wenzelm [Thu, 19 Jun 2008 20:48:05 +0200] rev 27281
Variable.declare_typ;
wenzelm [Thu, 19 Jun 2008 20:48:04 +0200] rev 27280
added declare_typ;
wenzelm [Thu, 19 Jun 2008 20:48:03 +0200] rev 27279
moved add_used to Isar/rule_insts.ML;
wenzelm [Thu, 19 Jun 2008 20:48:02 +0200] rev 27278
export read_typ/cert_typ -- version with regular context operations;
tuned;
wenzelm [Thu, 19 Jun 2008 20:48:01 +0200] rev 27277
export read_typ/cert_typ -- version with regular context operations;
wenzelm [Thu, 19 Jun 2008 20:48:00 +0200] rev 27276
tuned signature;
removed duplicate of RecordPackage.read_typ;
replaced Typetab by existing Typtab;
wenzelm [Thu, 19 Jun 2008 20:47:58 +0200] rev 27275
removed duplicate of DatatypePackage.read_typ;
huffman [Thu, 19 Jun 2008 20:34:28 +0200] rev 27274
add lemma cfcomp_LAM
wenzelm [Thu, 19 Jun 2008 17:32:18 +0200] rev 27273
add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);
urbanc [Thu, 19 Jun 2008 15:47:26 +0200] rev 27272
slightly tuned
krauss [Thu, 19 Jun 2008 11:46:14 +0200] rev 27271
generalized induct_scheme method to prove conditional induction schemes.
huffman [Thu, 19 Jun 2008 00:02:08 +0200] rev 27270
add lemma iterate_iterate
wenzelm [Wed, 18 Jun 2008 23:15:41 +0200] rev 27269
* Disposed old term read functions;
huffman [Wed, 18 Jun 2008 23:07:30 +0200] rev 27268
replace preorder class with locale
huffman [Wed, 18 Jun 2008 23:03:11 +0200] rev 27267
add lemma compact_imp_principal to locale ideal_completion
wenzelm [Wed, 18 Jun 2008 22:32:06 +0200] rev 27266
added type_constraint (formerly in type_infer.ML, which is now loaded later);
wenzelm [Wed, 18 Jun 2008 22:32:04 +0200] rev 27265
TypeExt.type_constraint;
wenzelm [Wed, 18 Jun 2008 22:32:03 +0200] rev 27264
simplified TypeInfer.infer_types;
wenzelm [Wed, 18 Jun 2008 22:32:02 +0200] rev 27263
improved error output -- variant/mark bounds;
simplified infer_types -- always freeze, no result substitution;
wenzelm [Wed, 18 Jun 2008 22:32:01 +0200] rev 27262
load type_infer.ML after Syntax module;
wenzelm [Wed, 18 Jun 2008 18:55:10 +0200] rev 27261
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm [Wed, 18 Jun 2008 18:55:08 +0200] rev 27260
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
read_term: imitate old behaviour (allow_dummies, mode_schematic);
wenzelm [Wed, 18 Jun 2008 18:55:07 +0200] rev 27259
export transfer_syntax;
added allow_dummies feature (for legacy emulations);
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm [Wed, 18 Jun 2008 18:55:06 +0200] rev 27258
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
wenzelm [Wed, 18 Jun 2008 18:55:05 +0200] rev 27257
removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
wenzelm [Wed, 18 Jun 2008 18:55:04 +0200] rev 27256
added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
wenzelm [Wed, 18 Jun 2008 18:55:03 +0200] rev 27255
removed obsolete read_def_cterms/read_cterm;
wenzelm [Wed, 18 Jun 2008 18:55:02 +0200] rev 27254
load proof term operations later;
wenzelm [Wed, 18 Jun 2008 18:55:01 +0200] rev 27253
more antiquotations;
wenzelm [Wed, 18 Jun 2008 18:55:00 +0200] rev 27252
OldGoals.read_prop;
wenzelm [Wed, 18 Jun 2008 18:54:59 +0200] rev 27251
OldGoals.simple_read_term;
wenzelm [Wed, 18 Jun 2008 18:54:57 +0200] rev 27250
simplified Abel_Cancel setup;
wenzelm [Wed, 18 Jun 2008 16:55:44 +0200] rev 27249
updated generated file;
wenzelm [Wed, 18 Jun 2008 16:55:21 +0200] rev 27248
pervasive cut_inst_tac;
urbanc [Tue, 17 Jun 2008 04:19:50 +0200] rev 27247
added a progress lemma and tuned some comments
wenzelm [Mon, 16 Jun 2008 22:20:59 +0200] rev 27246
* Rules and tactics that read instantiations now demand a proper context;