equal
deleted
inserted
replaced
5 (* Core Haskell *) |
5 (* Core Haskell *) |
6 |
6 |
7 atom_decl var |
7 atom_decl var |
8 atom_decl cvar |
8 atom_decl cvar |
9 atom_decl tvar |
9 atom_decl tvar |
10 |
|
11 declare [[STEPS = 31]] |
|
12 |
10 |
13 nominal_datatype core_haskell: |
11 nominal_datatype core_haskell: |
14 tkind = |
12 tkind = |
15 KStar |
13 KStar |
16 | KFun "tkind" "tkind" |
14 | KFun "tkind" "tkind" |
95 thm core_haskell.bn_defs |
93 thm core_haskell.bn_defs |
96 thm core_haskell.perm_simps |
94 thm core_haskell.perm_simps |
97 thm core_haskell.eq_iff |
95 thm core_haskell.eq_iff |
98 thm core_haskell.fv_bn_eqvt |
96 thm core_haskell.fv_bn_eqvt |
99 thm core_haskell.size_eqvt |
97 thm core_haskell.size_eqvt |
|
98 thm core_haskell.supp |
100 |
99 |
101 (* |
100 (* |
102 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
101 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
103 unfolding fresh_star_def Ball_def |
102 unfolding fresh_star_def Ball_def |
104 by auto (simp_all add: fresh_minus_perm) |
103 by auto (simp_all add: fresh_minus_perm) |