1994-09-09 lcp 1994-09-09 Per cent (%) now functions as comment character in tt box environment
1994-09-09 lcp 1994-09-09 Added mention of directory IMP; tidied the section on examples.
1994-09-09 lcp 1994-09-09 Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the datatype declaration and 7 on (co)inductive definitions. Added mention of directory IMP.
1994-09-09 lcp 1994-09-09 ZF/Zorn/next_bounded: deleted this proof, which was already in comments
1994-09-08 lcp 1994-09-08 documentation on theories
1994-09-08 lcp 1994-09-08 ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
1994-09-08 lcp 1994-09-08 {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
1994-09-07 lcp 1994-09-07 addition of ZF/ex/twos_compl.thy
1994-09-07 clasohm 1994-09-07 moved from Contrib
1994-09-07 clasohm 1994-09-07 renamed temporary variable 'base' to 'thy' in mk_structure
1994-09-06 clasohm 1994-09-06 renamed base_on into mk_base and moved it to the beginning of the generated .thy.ML file to make sure that all base theories are present when ML executes the rest of this file
1994-09-06 lcp 1994-09-06 Pure/type/unvarifyT: moved there from logic.ML
1994-09-06 lcp 1994-09-06 documentation of theory sections (co)inductive and (co)datatype
1994-09-06 wenzelm 1994-09-06 minor internal changes;
1994-09-06 wenzelm 1994-09-06 added ext_tsig_types; various minor changes;
1994-09-06 lcp 1994-09-06 removal of needless quotes
1994-08-31 nipkow 1994-08-31 Updated datatype documentation with a few hints
1994-08-25 lcp 1994-08-25 new file of useful things for writing theory sections
1994-08-25 lcp 1994-08-25 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils
1994-08-25 lcp 1994-08-25 print_sign_exn: now exported, with a polymorphic type
1994-08-24 lcp 1994-08-24 ZF/ex/LList/lconst_type: streamlined proof
1994-08-23 wenzelm 1994-08-23 added print_syntax: theory -> unit;
1994-08-23 wenzelm 1994-08-23 read_def_cterm: minor changes; merge_thm_sgs: improved error msg;
1994-08-23 wenzelm 1994-08-23 removed constant _constrain from Pure sig;
1994-08-22 lcp 1994-08-22 ZF/upair/consE', UnE': new
1994-08-22 lcp 1994-08-22 ZF/Cardinal: some results moved here from CardinalArith ZF/CardinalArith/nat_succ_lepoll: removed obsolete proof ZF/CardinalArith/nat_cons_eqpoll: new
1994-08-22 lcp 1994-08-22 Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens, brackets, ..., mk_triple
1994-08-22 lcp 1994-08-22 HOLCF/Lift1.thy: now imports Sum
1994-08-19 wenzelm 1994-08-19 replaced Lexicon.scan_id by Scanner.scan_id; replaced const_name by Syntax.const_name;
1994-08-19 wenzelm 1994-08-19 replaced add_defns_i by add_defs_i;
1994-08-19 wenzelm 1994-08-19 replaced sextension.ML by syn_trans.ML;
1994-08-19 wenzelm 1994-08-19 slightly changed args of infer_types; replaced parents by enclose; renamed 2nd add_types to attach_types and fixed the typevar-sort-constraint BUG; various minor internal changes;
1994-08-19 wenzelm 1994-08-19 added inferT_axm; removed extend_theory; changed read_def_cterm: now uses Sign.infer_types;
1994-08-19 wenzelm 1994-08-19 replaced mapst by map; added find_first;
1994-08-19 wenzelm 1994-08-19 added pretty_sg; added infer_types; removed subclasses arg of add_classes; removed old 'extend' and related stuff; various minor internal changes;
1994-08-19 wenzelm 1994-08-19 added add_defs, add_defs_i;
1994-08-19 wenzelm 1994-08-19 cleaned sig; removed add_defns (now in drule.ML as add_defs); removed add_sigclass; minor internal changes;
1994-08-19 wenzelm 1994-08-19 added theory_of_sign, theory_of_thm; renamed get_thms to thms_of; improved store_thms etc.;
1994-08-19 wenzelm 1994-08-19 renamed 'defns' to 'defs'; removed 'sigclass'; replaced parents by enclose; exported parens, brackets, mk_list, mk_big_list, mk_pair, mk_triple; various minor internal changes;
1994-08-19 wenzelm 1994-08-19 added raw_term_sorts and changed typ_of_term accordingly (part of fix of the typevar-sort-constraint BUG); various minor internal changes;
1994-08-19 wenzelm 1994-08-19 added type xrule (from sextension.ML); removed old 'extend'; removed added syn_ext_const_names, syn_ext_trfuns (now in syn_ext.ML); various minor changes;
1994-08-19 wenzelm 1994-08-19 removed idT, varT, tidT, tvarT (now in lexicon.ML); added syn_ext_const_names, syn_ext_trfuns;
1994-08-19 wenzelm 1994-08-19 various minor internal changes;
1994-08-19 wenzelm 1994-08-19 added map_strs: (string -> string) -> T -> T;
1994-08-19 wenzelm 1994-08-19 removed roots arg of extend_gram; added functor sig constraint (: PARSER);
1994-08-19 wenzelm 1994-08-19 minor cleanings;
1994-08-19 wenzelm 1994-08-19 replaced id, var, tid, tvar by idT, varT, tidT, tvarT; added const, free, var: build atomic terms of dummyT; added 'xnum' (signed numerals) and 'xstr' (strings) token kinds; various minor internal changes;
1994-08-19 wenzelm 1994-08-19 replaced SExtension by SynTrans (mixfix stuff in Mixfix); private structs now hidden within PrivateSyntax;
1994-08-19 wenzelm 1994-08-19 added this file;
1994-08-19 lcp 1994-08-19 deleted obsolete references to ISABELLEMAKE
1994-08-18 lcp 1994-08-18 /unvarifyT, unvarify: moved to Pure/logic.ML
1994-08-18 lcp 1994-08-18 Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved from prove_goalw
1994-08-18 lcp 1994-08-18 Pure/library/assert_all: new, moved from ZF/ind_syntax.ML
1994-08-18 lcp 1994-08-18 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML ZF/ind_syntax/prove_term: deleted ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and Logic.unvarify
1994-08-18 lcp 1994-08-18 HOLCF/Lift1.thy: updated for new sum_case by using "case" syntax
1994-08-17 lcp 1994-08-17 overheads for inductive definitions, originally for CADE-12
1994-08-17 lcp 1994-08-17 ZF/ex/ROOT: added .ML to use command use "ex/twos_compl" Should be able to delete this after fixing the treatment of orphans.
1994-08-17 lcp 1994-08-17 ZF/ex/Ntree: two new examples, maptree and maptree2
1994-08-17 lcp 1994-08-17 ZF/func/fun_extend3: new ZF/func/cons_fun_eq: simplified proof
1994-08-17 lcp 1994-08-17 ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted