moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; moved generic definitions about relations from Quotient.thy to Predicate; consistent use of R rather than E for relations; more natural deduction rules

moved generic definitions about relations from Quotient.thy to Predicate; more natural deduction rules

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; more natural deduction rules; replaced slightly odd locale equiv by plain definition

simplify proof of LIMSEQ_unique

use new 'file' antiquotation for reference to Dedekind_Real.thy

merged

instance list :: (discrete_cpo) discrete_cpo; compactness lemmas for Nil, Cons; instance list :: (chfin) chfin;

merged

also support higher-order rules for Z3 proof reconstruction

merged

less ghc-specific pragma

tuned

updated generated files;

added document antiquotation @{file};

Parse.liberal_name for document antiquotations and attributes;

ML results: enter before printing (cf. Poly/ML SVN 1218);

merged

merged

merged

change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec

add lemma cont2cont_if_bottom

added Parse.literal_fact with proper inner_syntax markup (source position); tuned;

tuned signature;

less frequent sidekick parsing, which is relatively slow;

basic setup for bundled Java runtime;

updated reference platforms;

merged

merged

gave more standard finite set rules simp and intro attribute

more permissive Isabelle_System.mkdir; exported File.is_dir (weak test);