1995-03-21 clasohm 1995-03-21 changed syntax of Unity ("()" instead of "<>")
1995-03-20 clasohm 1995-03-20 converted IOA with curried function application
1995-03-20 clasohm 1995-03-20 changed syntax of "if"
1995-03-17 clasohm 1995-03-17 fixed two severe bugs in calc_xrules and case_rule
1995-03-17 nipkow 1995-03-17 Corrected a silly old bug in merge_tsigs. Rewrote a lot of Nimmermann's code.
1995-03-17 nipkow 1995-03-17 Added a few thms to nat_ss and list_ss
1995-03-17 regensbu 1995-03-17 Removed bugs which occurred due to new generation mechanism for type variables
1995-03-16 lcp 1995-03-16 Removed exception handlers, as they are now in ZF/Makefile.
1995-03-15 clasohm 1995-03-15 removed print_msg parameter of infer_types
1995-03-15 lcp 1995-03-15 Now mentions Coind
1995-03-15 lcp 1995-03-15 Removed exception handlers, as they are now in ZF/Makefile.
1995-03-15 lcp 1995-03-15 Now calls exit_use instead of use, for prompt failure if errors are detected.
1995-03-15 lcp 1995-03-15 Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).
1995-03-15 lcp 1995-03-15 Now the "use" call has an exception handler, for prompt failure if errors are detected.
1995-03-15 lcp 1995-03-15 Now calls exit_use instead of use, for prompt failure if errors are detected.
1995-03-14 nipkow 1995-03-14 Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.
1995-03-14 nipkow 1995-03-14 added exit 1
1995-03-13 nipkow 1995-03-13 Removed superfluous type constraint
1995-03-13 nipkow 1995-03-13 Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.
1995-03-11 nipkow 1995-03-11 Added type constraints to enforce correct choice of variable names.
1995-03-11 lcp 1995-03-11 Put freeze into the signature TACTIC for export
1995-03-10 lcp 1995-03-10 Removed "localize"; instead, proofs refer to their own assumptions.
1995-03-09 lcp 1995-03-09 Commented isof(c,t)
1995-03-08 nipkow 1995-03-08 Added dependencies on ../Provers/hypsubst.ML and removed those on ../Provers/ind.ML
1995-03-08 nipkow 1995-03-08 Replaced read by read_cterm.
1995-03-08 nipkow 1995-03-08 Enforced partial evaluation of mk_case_split_tac.
1995-03-08 nipkow 1995-03-08 Enforced partial evaluation of mk_case_split_tac
1995-03-08 nipkow 1995-03-08 Added dependencies on files in Provers
1995-03-08 nipkow 1995-03-08 Added pretty-printing coments
1995-03-07 nipkow 1995-03-07 *** empty log message ***
1995-03-07 nipkow 1995-03-07 *** empty log message ***
1995-03-07 nipkow 1995-03-07 Hoare logic
1995-03-07 lcp 1995-03-07 Changed Univ to Datatype in parents
1995-03-07 lcp 1995-03-07 Replaced rules by defs. Also got rid of tyconstU by including TyConst in the datatype's universe
1995-03-07 lcp 1995-03-07 Replaced rules by defs
1995-03-07 lcp 1995-03-07 Got rid of exvarU and constU by including ExVar and Const in various datatype universes.
1995-03-07 lcp 1995-03-07 Deleted constQU, exvarQU, expQU by including Const, ExpVar, Exp in Value.thy's codatatype declaration.
1995-03-07 lcp 1995-03-07 Replaced rules by defs
1995-03-07 lcp 1995-03-07 Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.
1995-03-07 lcp 1995-03-07 Moved declaration of ~= to a syntax section
1995-03-03 clasohm 1995-03-03 replaced Pure by ProtoPure
1995-03-03 clasohm 1995-03-03 fixed a bug in infer_types/exn_type_msg
1995-03-03 clasohm 1995-03-03 new version of HOL/Integ with curried function application
1995-03-03 clasohm 1995-03-03 new version of HOL/IMP with curried function application
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-03-02 wenzelm 1995-03-02 added declaration of syntactic const "_abs";
1995-02-28 lcp 1995-02-28 Added initial /bin/csh line and comments
1995-02-28 lcp 1995-02-28 No longer calls maketest; instead, the Makefile writes the file test.
1995-02-28 lcp 1995-02-28 Uses "suffix substitution" to shorten macro definitions.
1995-02-28 lcp 1995-02-28 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.
1995-02-28 lcp 1995-02-28 New example by Jacob Frost, tidied by lcp
1995-02-27 lcp 1995-02-27 New example by Jacob Frost, tidied by lcp
1995-02-27 lcp 1995-02-27 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.
1995-02-27 lcp 1995-02-27 Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)
1995-02-27 lcp 1995-02-27 Redefined functions to suppress redundant leading 0s and 1s
1995-02-27 wenzelm 1995-02-27 new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;
1995-02-27 lcp 1995-02-27 Added the exception handler handle _ => exit 1. This will catch all errors and force an exit with error code, causing Make to fail.
1995-02-27 lcp 1995-02-27 intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ
1995-02-27 lcp 1995-02-27 Updated comment about list_subset_univ and list_into_univ.