QuotMain.thy
changeset 182 c7eff9882bd8
parent 180 fcacca9588b4
child 185 929bc55efff7
--- a/QuotMain.thy	Sat Oct 24 22:52:23 2009 +0200
+++ b/QuotMain.thy	Sun Oct 25 00:14:40 2009 +0200
@@ -164,15 +164,6 @@
   maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
 *}
 
-
-ML {* quotdata_lookup @{theory} *}
-setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*}
-ML {* quotdata_lookup @{theory} *}
-
-ML {* print_quotdata @{context} *}
-
-ML {* maps_lookup @{theory} @{type_name list} *}
-
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let