src/FOL/FOL.ML

turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.

structure FOL =
struct
  val thy = the_context ();
  val classical = classical;
end;

AddXIs [equal_intr_rule, disjI1, disjI2];

open FOL;