(* NOTE - this file linked multiple places, careful when editing *) structure OldGoals = Goals ; add_path "$ISABELLE_HOME_USER/2005/gen" ; add_path "$ISABELLE_HOME_USER/2005/pmgms" ; val () = ThyLoad.add_path "$ISABELLE_HOME/src/HOL/Lattice" ; add_path "../cdeep" ; (* add_path "../fdeep" ; *) show_path(); use_thy "stringSyntax" ; (* to get noprefs *) fun ufdf _ = update_thy "Fdefs" ; fun ufs _ = update_thy "Fsame" ; fun ufe _ = update_thy "Fextra" ; fun ufd _ = update_thy "Fder" ; fun und _ = update_thy "Ndefs" ; fun undis _ = update_thy "N_Display" ; fun unr _ = update_thy "N_Rls" ; fun uds _ = update_thy "Dc_Sn" ; fun undp _ = update_thy "Ndeep" ; fun unm _ = update_thy "Ns_Ms" ; fun um _ = update_thy "Msde" ; fun uc _ = update_thy "Ctxt" ; fun ur _ = update_thy "Rotate" ; fun ucr _ = update_thy "CRotate" ; fun up2 _ = update_thy "P2Rotate" ; fun upr _ = update_thy "Prop_Rotate" ; fun ufr _ = update_thy "Finish_Rotate" ; fun udn _ = update_thy "Dc_Nested" ; fun ua _ = update_thy "all" ; fun uge _ = update_thy "GElim" ; (* requires ../cdeep in path *) fun ucec _ = update_thy "CE_Conds" ; fun uhc8 _ = update_thy "HOL_C8" ; fun ufc8 _ = update_thy "fC8cases" ; fun ufc _ = update_thy "F_Cut" ; fun uca _ = update_thy "F_Cat" ; fun unc _ = update_thy "N_Cat" ; fun ud _ = update_thy "Display" ; fun ua _ = update_thy "all" ;