2000-07-13 wenzelm 2000-07-13 bind_skolem;
2000-07-13 wenzelm 2000-07-13 invoke_case: bind_skolem;
2000-07-13 wenzelm 2000-07-13 "_i" arguments now expected to have skolems already internalized; removed unused cert_skolem, export intern_skolem, added bind_skolem;
2000-07-13 wenzelm 2000-07-13 make: opaq flag;
2000-07-13 wenzelm 2000-07-13 added internal, dest_internal;
2000-07-12 wenzelm 2000-07-12 infix 'OF' is a version of 'MRS' with more appropriate argument order;
2000-07-12 kleing 2000-07-12 about.html -> logics.html
2000-07-12 kleing 2000-07-12 munich webserver is now sunbroy51
2000-07-12 kleing 2000-07-12 about -> logics, better access to online libraries
2000-07-10 paulson 2000-07-10 removal of (harmless) circular definitions
2000-07-09 berghofe 2000-07-09 Tuned proof.
2000-07-08 nipkow 2000-07-08 Defs are now checked for circularity (if not overloaded).
2000-07-07 wenzelm 2000-07-07 inter_sort: keep normal!
2000-07-07 nipkow 2000-07-07 Tightened up check of types in constant defs.
2000-07-07 nipkow 2000-07-07 added type classes to constant's type
2000-07-07 bauerg 2000-07-07 skp; le;
2000-07-07 oheimb 2000-07-07 added dependency caveat
2000-07-07 oheimb 2000-07-07 added dependency caveat
2000-07-07 oheimb 2000-07-07 added IMP/Examples.ML dependence
2000-07-06 wenzelm 2000-07-06 tuned msgs;
2000-07-06 wenzelm 2000-07-06 allow comment in more commands;
2000-07-06 wenzelm 2000-07-06 Isabelle99-1;
2000-07-06 kleing 2000-07-06 ADD -> IAdd
2000-07-06 nipkow 2000-07-06 Removed some junk thms.
2000-07-06 nipkow 2000-07-06 added zabs to arith_tac
2000-07-06 nipkow 2000-07-06 Deleted list_case thms no subsumed by case_tac
2000-07-06 nipkow 2000-07-06 Now two split thms for same constant at different types is allowed.
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 bauerg 2000-07-06 removed sorry;
2000-07-06 bauerg 2000-07-06 removed sorry;
2000-07-06 kleing 2000-07-06 new ADD instruction
2000-07-06 paulson 2000-07-06 removal of batch style, and tidying
2000-07-06 paulson 2000-07-06 fixed typos reported by Jeremy Dawson
2000-07-06 bauerg 2000-07-06 added;
2000-07-06 bauerg 2000-07-06 completed TYPES version of HahnBanach;
2000-07-06 nipkow 2000-07-06 *** empty log message ***
2000-07-06 wenzelm 2000-07-06 Compatibility file for Moscow ML 2.00;
2000-07-06 wenzelm 2000-07-06 run Moscow ML 2.00 --- does not handle saved images (yet!?);
2000-07-06 wenzelm 2000-07-06 Moscow ML 2.00 or later (experimental!); tuned;
2000-07-05 paulson 2000-07-05 more tidying. also generalized some tactics to prove "Type A" and "a = b : A" judgements
2000-07-05 oheimb 2000-07-05 disambiguated := ; added Examples (factorial)
2000-07-05 paulson 2000-07-05 removed batch proofs
2000-07-05 paulson 2000-07-05 massive tidy-up: goal -> Goal, remove use of prems, etc.
2000-07-05 oheimb 2000-07-05 disambiguated := ; added Examples (factorial)
2000-07-05 oheimb 2000-07-05 corrected symbol for casting relation
2000-07-04 paulson 2000-07-04 removed most batch-style proofs
2000-07-04 wenzelm 2000-07-04 tuned;
2000-07-04 oheimb 2000-07-04 disambiguated := ; added Examples (factorial)
2000-07-04 nipkow 2000-07-04 added a thm.
2000-07-04 oheimb 2000-07-04 disambiguated := ; added Examples (factorial)
2000-07-04 oheimb 2000-07-04 added BinOp
2000-07-04 wenzelm 2000-07-04 * added 'nothing' --- the empty list of theorems;
2000-07-04 wenzelm 2000-07-04 added "nothing" (empty list of theorems);
2000-07-04 wenzelm 2000-07-04 fixed usage;
2000-07-04 wenzelm 2000-07-04 tuned comments; even smarter guessing of ProofGeneral location;
2000-07-03 wenzelm 2000-07-03 previde 'defs' field for quick_and_dirty;
2000-07-01 wenzelm 2000-07-01 IGNORE last log message! added antiquote options "long_names", "eta_contract";