Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST, REPEAT_DETERM_SOME: new

FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM

argument swaps in HOL

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.

updated pathnames

updated discussion of congruence rules in first section

changed warning for extremely ambiguous expressions

Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final result.

ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)

ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)

ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E ZF/Perm/comp_fun: tidied; removed use of PiI

ZF/InfDatatype/fun_Vcsucc: removed use of PiE

ZF/func: tidied many proofs, using new definition of Pi(A,B) ZF/func/PiI,PiE: removed ZF/func/Pi_iff_old: new ZF/func/Pi_memberD: new; simpler, replaces memberPiE

ZF: NEW DEFINITION OF PI(A,B) Was Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f} Now function(r) == ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y') Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" This simplifies many proofs, since (a) the top-level definition has fewer bound variables (b) the "total" and "function" properties are separated (c) the awkward EX! quantifier is eliminated. ZF/ZF.thy/function: new definition

ZF/Fixedpt/subset_cs: moved to ZF/subset.ML

ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML

ZF/domrange/converse_iff: new

ZF/upair/theI2: new

ZF/equalities/domain_converse,range_converse, prod_Un_distrib2,prod_Int_distrib2: new

ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML ZF/Fixedpt/subset_cs: moved to ZF/subset.ML

Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE

added warning message "Currently parsed expression could be extremely ambiguous."

Provers/classical: now takes theorem "classical" as argument, proves "swap" Provers/classical/depth_tac,deepen_tac: new

Provers/hypsubst: greatly simplified! No longer simulates a "eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen equality to the end!

Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of exception TYPE

Modified pattern.ML to perform proper matching of Higher-Order Patterns. Modified thm.ML to preserve bound var names during rewriting. Renamed eta_matches to matches.

FOL/FOL/swap: deleted FOL/FOL: tidied the signature

HOLCF/Ssum3.ML: changed res_inst_tac [("P"... to res_inst_tac [("Pa" in some very ugly proofs. Needed to handle new variable names in swap.

ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}

ZF/domrange/image_subset: tidied

ZF/upair/mem_asym,succ_inject: tidied

com1,2: added simplifier calls to remove use of ssubst in fast_tac

Pure/tctical/THEN_ELSE: new

Pure/tactic/build_netpair: now takes two arguments

Pure/sequence/hd,tl: new

Pure/drule/thin_rl: new

FOL/ex/ROOT: now loads mini.ML

FOL/ROOT/FOL_dup_cs: removed as obsolete FOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac

FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs

ZF/ZF/ex1_functional: moved to FOL/ROOT

Miniscope conversoin; example of formula rewriting

ZF/OrderArith/thin: deleted as obsolete ZF/OrderArith/wf_on_radd: now uses thin_rl

added final newline

added header files; deleted commented-out code

Prepared the code for preservation of bound var names during rewriting. Still requires a matching function for HO-patterns.

removed superfluous type_intrs in datatype com.

simplified syntax of infix continuous functiuons

strip_quotes now exported;

minor change of occs_const in dest_defn;

added require_thy;

HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities. constructor ";" now yields a low precedence; the reduction relations are now more like infixes.

ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive definitions may involve ordinary pairs. (HOL/intr_elim does not require this change)

Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse to simplfy %x y.?a(x) =?= %x y.?b(f(?c(y), y)) because it found the flexible path to y before the rigid path. New code simplifies this to %x.?a(x) =?= %x.?d, eliminating ?a. Pure/Unify/rigid_bound: preliminary check for rigid paths to the banned bound variables Pure/Unify/change_bnos: any occurrences of the banned bound variables must now be flexible, causing abandonment of the "cleaning"

LK/hardquant/37: deleted call to flexflex_tac: no longer needed

LCF/LCF.thy: the constant VOID had mixfix syntax "()" !! Added quotes.

FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities. Now proof objects have high precedences. Eliminates ambiguity in a=b:P being parsed as (a=b):P.

ZF/Fixedpt/coinduct: modified proof to suppress deep unification

new comments explaining abandoned change

LCF/fix/lfp_is_FIX: modified proof to suppress deep unification

FOL/ex/cla/58: slightly shorter proof

trivial update to reference

CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification CCL/CCL, Fix, Gfp, Hered, Set, Term, Trancl, Type, Wfd: expanded shorthands

add_defs: improved error messages; installed new print_goals with nice 'env mode';

removed old comment;

remove _explode, _implode and trfuns;

prove_subclass, prove_arity now exported; minor internal changes;

added is_equals: term -> bool;

type_args, opt_witness now exported; added AxClass.;

AxClass no longer open;

{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully

{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

fixed infix names in print_translations;

Pure/tctical/suppress_tracing: new; can now switch tracing off until the next tactical call. There is no good way of doing this because of backtracking. Pure/tctical/exec_trace_command,tracify,traced_tac: these set, test and reset suppress_tracing

Minor reference updates

Moving theory LList to ex directory

corrected problems with changed binding power of ::.

README file

changed precedences of _constrain (i.e. "::")

New version

made major changes to grammar; added call of Type.infer_types to automatically eliminate ambiguities

added print_msg; added call of Type.infer_types to resolve ambiguities

Modified termord to take account of the Abs-Abs case.

improved expand_typ (now handles TVars); slightly changed ext_tsig_abbrs; added ext_tsig_arities; removed extend_tsig; various internal changes;

exported pretty_sort; various minor internal changes;

added init_pps;

added init_database (somewhat experimental);

added flag show_no_free_types: bool ref;

explode_tr now produces leadings 0s; implode_ast_tr' now quotes result;

minor cleanup, added 'syntax' section;

now mentions that the sections are available as Datatypes and (Co)Inductive Definitions in Isabelle/HOL

removed lookup_const (use Sign.const_type instead);

replaced lookup_const by Sign.const_type;

now uses Sign.const_type;

letrec syntax: replaced "id" by "idt";

updated for Isabelle94

now uses find to locate .thy.ML files everywhere

updated the identifier "version"

minor updates

New Makefile for Logics Manual

New Makefile for Reference Manual

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