1997-11-05 paulson [Wed, 05 Nov 1997 13:23:46 +0100] rev 4153
Ran expandshort, especially to introduce Safe_tac
src/HOL/Auth/Yahalom2.ML src/HOL/AxClasses/Lattice/CLattice.ML src/HOL/AxClasses/Lattice/LatInsts.ML src/HOL/AxClasses/Lattice/LatMorph.ML src/HOL/AxClasses/Lattice/LatPreInsts.ML src/HOL/AxClasses/Lattice/Lattice.ML src/HOL/AxClasses/Lattice/OrdDefs.ML src/HOL/AxClasses/Lattice/Order.ML src/HOL/Finite.ML src/HOL/Hoare/Examples.ML src/HOL/Hoare/List_Examples.ML src/HOL/IMP/Hoare.ML src/HOL/IMP/Transition.ML src/HOL/IOA/IOA.ML src/HOL/IOA/Solve.ML src/HOL/MiniML/Generalize.ML src/HOL/MiniML/Instance.ML src/HOL/MiniML/Type.ML src/HOL/NatDef.ML src/HOL/Subst/Unify.ML src/HOL/Trancl.ML src/HOL/Univ.ML src/HOL/WF.ML src/HOL/ex/MT.ML src/HOL/ex/Primrec.ML src/HOL/ex/cla.ML src/HOL/ex/meson.ML src/HOL/ex/set.ML

1997-11-05 paulson [Wed, 05 Nov 1997 13:14:15 +0100] rev 4152
Ran expandshort, especially to introduce Safe_tac
src/ZF/AC/AC10_AC15.ML src/ZF/AC/WO2_AC16.ML src/ZF/AC/WO6_WO1.ML src/ZF/AC/rel_is_fun.ML src/ZF/Cardinal.ML src/ZF/CardinalArith.ML src/ZF/Coind/ECR.ML src/ZF/Coind/MT.ML src/ZF/Coind/Map.ML src/ZF/EquivClass.ML src/ZF/Finite.ML src/ZF/IMP/Equiv.ML src/ZF/Order.ML src/ZF/OrderArith.ML src/ZF/OrderType.ML src/ZF/Ordinal.ML src/ZF/Perm.ML src/ZF/Resid/Confluence.ML src/ZF/Resid/Cube.ML src/ZF/Resid/Reduction.ML src/ZF/Resid/Residuals.ML src/ZF/Resid/SubUnion.ML src/ZF/Univ.ML src/ZF/Zorn.ML src/ZF/ex/Integ.ML src/ZF/ex/LList.ML src/ZF/ex/Limit.ML src/ZF/ex/Mutil.ML src/ZF/ex/Ntree.ML src/ZF/ex/Primes.ML src/ZF/ex/Primrec.ML src/ZF/ex/PropLog.ML src/ZF/ex/Ramsey.ML src/ZF/ex/Term.ML src/ZF/ex/misc.ML

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:49:34 +0100] rev 4151
adapted typed_print_translation;
src/HOL/List.thy src/HOL/Set.thy

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:49:07 +0100] rev 4150
tuned record_info;
src/HOL/thy_data.ML

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:45:51 +0100] rev 4149
fixed exception OPTION;
TFL/tfl.sml src/Provers/blast.ML

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:43:37 +0100] rev 4148
adapted pure_trfunsT;
added type_tr/tr';
eliminated mk_ofclassS_tr';
src/Pure/Syntax/syn_trans.ML

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:42:19 +0100] rev 4147
print translation: added show_sorts argument;
src/Pure/Syntax/printer.ML

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:41:46 +0100] rev 4146
adapted syn_ext_trfunsT;
src/Pure/Syntax/syn_ext.ML

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:41:18 +0100] rev 4145
adapted extend_trfunsT;
src/Pure/Syntax/syntax.ML

1997-11-05 wenzelm [Wed, 05 Nov 1997 11:40:51 +0100] rev 4144
fixed exception OPTION;
src/Pure/Syntax/symbol_font.ML