Changes due to new abel_cancel.ML

use both processors on macbroy5

switch mac test to macbroy5

cleaned up

cleaned up proof of contlub_abstraction

meson method taking an argument list

deleted a redundant "use" line

tidying

stylistic tweaks concerning Find

shortened time out by 3h (gives up at 12:00h now). test should be finished by 10:00h usually.

made su[bp]/isu[bp] behave the same as their bsu[bp]..esu[bp] counterparts, properly respect isastylescript now

needed for Isabelle independent build

added theorems fix_strict, fix_defined, fix_id, fix_const

add binder syntax for flift1

add new file to test fixrec package

add csplit3, ssplit3, fup3 as simp rules

New features: permissive option for fixrec to skip proofs of equations; side conditions for fixrec equations (for definedness); fixpat theorem names apply to entire group of theorems; improved error messages

added match functions for spair, sinl, sinr

fixed \<Prod> syntax

new

Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers. Will now signal if ATP has run out of time and then kill the watcher.

* Pure: the Isar proof context type is already defined early in Pure as Context.proof;

added find2

*** empty log message ***

tunes Find

added Rules/find2

tuned pointer_eq;

renamed data kind;

removed proof data (see Pure/context.ML);

added depth_of;

removed obsolete object.ML (see Pure/library.ML);

export sort_ord; tuned term_ord, typ_ord: use pointer_eq; tuned aconv, aconvs: based on term_ord;

renamed init to init_data;

added structure Object (from Pure/General/object.ML);

tuned;

begin_thy: merge maximal imports; incorporate proof data; added generic context;

removed Pure/Isar/proof_data.ML, Pure/General/object.ML;

improved proof;

obsolete (see Pure/context.ML);

tuned;

pointer equality for sml/nj

(initial commit)

(initial commit)

(initial commit)

(initial commit)

*** empty log message ***

tuned

added -H false