add -p 2 at-sml-dev test for HOL proof terms sessions only

at-sml-dev session with -p 2

Added target for proof term sessions (those that need -p 2)

accept single logic and target as argument

exported constraint interfaces

exported intern_expr

added ocaml strings

further localization

proper syntax during class specification

prove_strong_ind now uses InductivePackage.rulify.

Adapted to changes in interface of add_inductive_i.

add_inductive_i now takes typ instead of typ option as argument.

- add_inductive_i now takes typ instead of typ option as argument - close_rule is now applied before expanding abbreviations - rulify applies norm_hhf again

proper handling of chained facts;

removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions

Fixed setup of transitivity reasoner (function decomp).

some more simultaneous use_thys;

read: explicit treatment of scanner failure;

tuned;

tuned;

tuned;

* Pure/Isar: unified specification syntax admits type inference and dummy patterns; print mode: no_abbrevs;

read/check_specification: free_dummy_patterns;

added free_dummy_patterns;

added minimize_sort, complete_sort;

Sign.minimize/complete_sort;

convenient obtain rule for sets

added code lemma for 1

moved Finite_Set before Datatype

adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);