src/Doc/Tutorial/Datatype/unfoldnested.thy
author paulson <lp15@cam.ac.uk>
Mon, 17 Jan 2022 17:04:50 +0000
changeset 74985 ac3901e4e0a9
parent 58860 fee7cfa69c50
permissions -rw-r--r--
A new lemma about inverse image
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8751
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
     1
(*<*)
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
     2
theory unfoldnested imports Main begin
8751
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
     3
(*>*)
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 8751
diff changeset
     4
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
6852682eaf16 *** empty log message ***
nipkow
parents: 8751
diff changeset
     5
and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
8751
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
     6
(*<*)
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
     7
end
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
     8
(*>*)