tuned
authorChristian Urban <urbanc@in.tum.de>
Sat, 01 May 2010 09:14:25 +0100
changeset 2006 2ceec1b4b015
parent 2005 233bb805a4df
child 2007 7ee9a2fefc77
tuned
Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri Apr 30 16:31:43 2010 +0100
+++ b/Nominal/NewParser.thy	Sat May 01 09:14:25 2010 +0100
@@ -519,7 +519,7 @@
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
-thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros
+thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros[no_vars]
 
 nominal_datatype ty =
   Var "name"