IsaMakefile for HOL;

removed unused symbol_input.pl

The previous log message was wrong. The correct one is: generalized handling of type expressions, type variables and sorts

removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2

added cfst_strict and csnd_strict

factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss

added qed_goal_spec_mp and qed_goalw_spec_mp

added nat_induct2

fixed EXIT def;

repaired some proofs

little improvement for the handling of sort constraints: two non-identical explicit constriants are considered equal if they give the same set in different enumerations, e.g. {term,ord,ord} = {ord,term}

Isabelle make utility;

added ISABELLE_HTML;

added ISABELLE_HTML; fixed Poly/ML 2.x;

improved usage msg;

IsaMakefile for FOL;

minor modifications to accomodate IsaMakefile;

IsaMakefile for Pure Isabelle;

now refers to absolute paths of binaries;

fixed ML_HOME; chmod fix;

improved error handling;

Isabelle user settings sample;

major cleanup; added comments;

Poly/ML style prompts;

fixed Title;

added consistency comment

added consistency comment

repaired several proofs

corrected 8bit symbols

tuned read and write functions;

New tactics: prove_unique_tac and analz_induct_tac

New tactic: prove_unique_tac

Removed a rogue TAB

New tactic: prove_unique_tac

intro_tacsf: replaced ORELSE by APPEND in order to stop errors that arise when unconstrained equalities appear in the premises. Could cause runtimes to increase...

SML/NJ startup script (for 0.93).

fixed \<subseteq> input;

SML/NJ startup script (for 0.93).

added smlnj-0.93;

Compatibility file for Standard ML of New Jersey, version 1.07.

added needs_filtered_use;

added write_charnames';

now uses SymbolInput.use;

symbol_input.ML: Defines 'use' command with symbol input filtering.

added symbol_input.ML;

fixed comment;

fixed comments;

now passes ML_SYSTEM as ml_system;