Put freeze into the signature TACTIC for export

Removed "localize"; instead, proofs refer to their own assumptions.

Commented isof(c,t)

Added dependencies on ../Provers/hypsubst.ML and removed those on ../Provers/ind.ML

Replaced read by read_cterm.

Enforced partial evaluation of mk_case_split_tac.

Enforced partial evaluation of mk_case_split_tac

Added dependencies on files in Provers

Added pretty-printing coments

*** empty log message ***

*** empty log message ***

Hoare logic

Changed Univ to Datatype in parents

Replaced rules by defs. Also got rid of tyconstU by including TyConst in the datatype's universe

Replaced rules by defs

Got rid of exvarU and constU by including ExVar and Const in various datatype universes.

Deleted constQU, exvarQU, expQU by including Const, ExpVar, Exp in Value.thy's codatatype declaration.

Replaced rules by defs

Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.

Moved declaration of ~= to a syntax section

replaced Pure by ProtoPure

fixed a bug in infer_types/exn_type_msg

new version of HOL/Integ with curried function application

new version of HOL/IMP with curried function application

new version of HOL with curried function application

added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)

added declaration of syntactic const "_abs";

Added initial /bin/csh line and comments

No longer calls maketest; instead, the Makefile writes the file test.

Uses "suffix substitution" to shorten macro definitions.

Re-organised to perform the tests independently. Now test is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to refer to the right command for running the object-logic. Uses "suffix substitution" to shorten macro definitions.

New example by Jacob Frost, tidied by lcp

New example by Jacob Frost, tidied by lcp

Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.

Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)

Redefined functions to suppress redundant leading 0s and 1s

new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;

Added the exception handler handle _ => exit 1. This will catch all errors and force an exit with error code, causing Make to fail.

intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ

Updated comment about list_subset_univ and list_into_univ.

exit: new, for use in Makefiles

Redefined arithmetic to suppress redundant leading 0s and 1s renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.

Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.

Proved zadd_left_commute and zmult_left_commute to define zadd_ac and zmult_ac. Deleted add_cong, add_kill and add_left_commute_kill as unused. Defined zadd_simps, zminus_simps, zmult_simps and added them to integ_ss.

New shell script for finding orphan .ML files (those with no .thy file)

added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)

added check "length ts > 1" before printing ambiguity warning in infer_types

Improved test for looping rewrite rules.

replaced pair_ss by prod_ss

Improved check for looping conditional rewrite rules.

ID for the file

ID for the file

'get ID update working'

CVS: CVS:

CVS:

added qed, qed_goal[w]

added specification of csh as script interpreter

simplified elimination of chain productions

binder: optional body pri now [bracketted];

improved read_xrules: patterns no longer read twice; tuned read_typ;

*** empty log message ***

instance: now automatically includes defs of current thy node as witnesses;

binder: optional body pri now [bracketted];

added documentation of pwd

renamed Sign.ambiguity_level to Syntax.ambiguity_level

moved ambiguity_level from sign.ML to Syntax/syntax.ML

moved ambiguity_level to Syntax/syntax.ML

added documentation of Sign.ambiguity_level

added reference variable ambiguity_level to control ambiguity warnings

changed due to new .bib files

added optional body priority to binder declaration

Under RS added cross reference to bind_thm

documented slow_tac, slow_best_tac, depth_tac, deepen_tac

removed mention of FOL_dup_cs

\bibliography now includes crossref.bib

updates for Isabelle94-2

simplified get_thm a bit

Replaced ordermap_z_lepoll by ordermap_z_lt, which is stronger and has a simpler proof. Modified proof of ordermap_csquare_le accordingly.

README: Now documents to Tools directory

Deleted semicolon at the end of the qed_goal line, which was preventing not_emptyE from being proved.

some cosmetic changes

added documentation of bind_thm, qed, qed_goal, get_thm, thms_of and theory_of_thm

added optional precedence for body of binder; removed call to infer_types from read_xrules

quite a lot of minor and major revisions (inspecting theories, read_axm, cert_axm, grammar generation, lexical matters, macro examples, ...);

empty_def typo

Proved comp_lam.

Corrected indexing of *datatype

prove_fun now includes equalityI. Added the rewrite rules Collect_simps and UnInt_simps.

Proved sum_bij, sum_ord_iso_cong, prod_bij, prod_ord_iso_cong,singleton_prod_bij, singleton_prod_ord_iso, prod_sum_singleton_bij, prod_sum_singleton_ord_iso. Rotated conjunctions in radd_Inl_iff, radd_Inr_iff to be more suitable for rewriting.

Proved case_cong and case_case.

Renamed single_fun to singleton_fun.

Now also depends upon equalities.thy, allowing use of the equalities in standard simpsets.

Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps and UnInt_simps to ZF_ss. Added consI1 to ZF_typechecks.

Removed spurious comment about eq_cs

Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML

Now depends upon Bool, so that 1 and 2 are defined