ProgTutorial/Recipes/USTypes.thy
author griff
Tue, 21 Jul 2009 12:05:15 +0200
changeset 269 3e084d62885c
parent 211 d5accbc67e1b
child 346 0fea8b7a14a1
permissions -rw-r--r--
show the type of "x" in the formula
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
theory USTypes
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
imports Main
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
begin
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
211
d5accbc67e1b more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset
     7
section {* User Space Type-Systems (TBD) *}
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
end
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
  
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15