New Makefile for Introduction

New Makefile for ind-defs

Added primrec section

Added primrec section.

now in a format that could be published

added Abrial and Laffitte; Kunen; Winskel, etc.

Updated for existence of HOL version and infinitely branching datatypes

Per cent (%) now functions as comment character in tt box environment

Added mention of directory IMP; tidied the section on examples.

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.

ZF/Zorn/next_bounded: deleted this proof, which was already in comments

documentation on theories

ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal

{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

addition of ZF/ex/twos_compl.thy

moved from Contrib

renamed temporary variable 'base' to 'thy' in mk_structure

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

Pure/type/unvarifyT: moved there from logic.ML

documentation of theory sections (co)inductive and (co)datatype

minor internal changes;

added ext_tsig_types; various minor changes;

removal of needless quotes

Updated datatype documentation with a few hints

new file of useful things for writing theory sections

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

print_sign_exn: now exported, with a polymorphic type

ZF/ex/LList/lconst_type: streamlined proof

added print_syntax: theory -> unit;

read_def_cterm: minor changes; merge_thm_sgs: improved error msg;

removed constant _constrain from Pure sig;

ZF/upair/consE', UnE': new

ZF/Cardinal: some results moved here from CardinalArith ZF/CardinalArith/nat_succ_lepoll: removed obsolete proof ZF/CardinalArith/nat_cons_eqpoll: new

Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens, brackets, ..., mk_triple

HOLCF/Lift1.thy: now imports Sum

replaced Lexicon.scan_id by Scanner.scan_id; replaced const_name by Syntax.const_name;

replaced add_defns_i by add_defs_i;

replaced sextension.ML by syn_trans.ML;

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;

added inferT_axm; removed extend_theory; changed read_def_cterm: now uses Sign.infer_types;

replaced mapst by map; added find_first;

added pretty_sg; added infer_types; removed subclasses arg of add_classes; removed old 'extend' and related stuff; various minor internal changes;

added add_defs, add_defs_i;

cleaned sig; removed add_defns (now in drule.ML as add_defs); removed add_sigclass; minor internal changes;

added theory_of_sign, theory_of_thm; renamed get_thms to thms_of; improved store_thms etc.;

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;

added raw_term_sorts and changed typ_of_term accordingly (part of fix of the typevar-sort-constraint BUG); various minor internal changes;

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;

removed idT, varT, tidT, tvarT (now in lexicon.ML); added syn_ext_const_names, syn_ext_trfuns;

various minor internal changes;

added map_strs: (string -> string) -> T -> T;

removed roots arg of extend_gram; added functor sig constraint (: PARSER);

minor cleanings;

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;

replaced SExtension by SynTrans (mixfix stuff in Mixfix); private structs now hidden within PrivateSyntax;

added this file;

deleted obsolete references to ISABELLEMAKE

/unvarifyT, unvarify: moved to Pure/logic.ML

Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved from prove_goalw

Pure/library/assert_all: new, moved from ZF/ind_syntax.ML