src/LCF/LCF.thy

  WHEN   :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
  adm    :: "('a => o) => o"
  VOID   :: "void"               ("'(')")
  PAIR   :: "['a,'b] => 'a*'b"   ("(1<_,/_>)" [0,0] 100)
  COND   :: "[tr,'a,'a] => 'a"   ("(_ =>/ (_ |/ _))" [60,60,60] 60)
- "<<"   :: "['a,'a] => o"       (infixl 50)
+ less   :: "['a,'a] => o"       (infixl "<<" 50)
 
 axioms
   (** DOMAIN THEORY **)
 
   eq_def:        "x=y == x << y & y << x"

   adm_not_free adm_eq adm_less adm_not_less
   adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
 
 
 ML {*
-local
-  val adm_lemmas = thms "adm_lemmas"
-  val induct = thm "induct"
-in
   fun induct_tac v i =
-    res_inst_tac[("f",v)] induct i THEN REPEAT (resolve_tac adm_lemmas i)
-end
+    res_inst_tac[("f",v)] @{thm induct} i THEN
+    REPEAT (resolve_tac @{thms adm_lemmas} i)
 *}
 
 lemma least_FIX: "f(p) = p ==> FIX(f) << p"
   apply (tactic {* induct_tac "f" 1 *})
   apply (rule minimal)

   apply (simp add: expand_all_PROD)
   apply (rule 3)
   done
 
 ML {*
-local
-  val induct2 = thm "induct2"
-  val adm_lemmas = thms "adm_lemmas"
-in
-
 fun induct2_tac (f,g) i =
-  res_inst_tac[("f",f),("g",g)] induct2 i THEN
-  REPEAT(resolve_tac adm_lemmas i)
+  res_inst_tac[("f",f),("g",g)] @{thm induct2} i THEN
+  REPEAT(resolve_tac @{thms adm_lemmas} i)
+*}
 
 end
-*}
-
-end