propp: 'concl' patterns;
assumptions: tactics for non-goal export;
use Display.pretty_thm_no_hyps;
assm vs. assume vs. presume;
tuned type goal;
tuned print_goal;
relative exports, absolute export_thm rule;
transfer_facts;
tuned;
(* Title: HOLCF/dnat2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Additional constants for dnat
*)
Dnat2 = Dnat +
consts
iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
rules
iterator_def "iterator = fix[LAM h n f x.\
\ dnat_when[x][LAM m.f[h[m][f][x]]][n]]"
end
(*
iterator[UU][f][x] = UU
iterator[dzero][f][x] = x
n~=UU --> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]]
*)